1  /-
  2  Copyright (c) 2018 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Kenny Lau
  5  
  6  Dependent functions with finite support (see `data/finsupp.lean`).
  7  -/
  8  
  9  import data.finset data.set.finite algebra.big_operators algebra.module algebra.pi_instances
src         └─────────┘ └─────────────┘ └───────────────────┘ └────────────┘ └──────────────────┘
 10  
 11  universes u u₁ u₂ v v₁ v₂ v₃ w x y l
 12  
 13  variables (ι : Type u) (β : ι → Type v)
id                  └──┘           
typ                 └──┘           
 14  
 15  def decidable_zero_symm {γ : Type w} [has_zero γ] [decidable_pred (eq (0 : γ))] : decidable_pred (λ x, x = (0:γ)) :=
id                                         └──────┘    └────────────┘  └┘            └────────────┘           
src                                        └──────┘     └────────────┘  └┘             └────────────┘         
typ                                        └──────┘    └────────────┘  └┘            └────────────┘           
 16  λ x, decidable_of_iff (0 = x) eq_comm
id       └──────────────┘       └─────┘
src       └──────────────┘        └─────┘
typ      └──────────────┘       └─────┘
 17  local attribute [instance] decidable_zero_symm
id                              └─────────────────┘
src                             └─────────────────┘
typ                             └─────────────────┘
 18  
 19  namespace dfinsupp
 20  
 21  variable [Π i, has_zero (β i)]
id                 └──────┘    
src                 └──────┘
typ                └──────┘    
 22  
 23  structure pre : Type (max u v) :=
 24  (to_fun : Π i, β i)
id                  
typ                 
 25  (pre_support : multiset ι)
id                  └──────┘ 
src                 └──────┘
typ                 └──────┘ 
doc                 └──────┘
 26  (zero : ∀ i, i ∈ pre_support ∨ to_fun i = 0)
id                 └─────────┘  └────┘  
src                                        
typ                └─────────┘  └────┘  
 27  
 28  instance : setoid (pre ι β) :=
id              └────┘  └─┘  
src             └────┘  └─┘
typ             └────┘  └─┘  
 29  { r := λ x y, ∀ i, x.to_fun i = y.to_fun i,
id                   └─────┘   └─────┘ 
src                      └─────┘     └─────┘
typ                  └─────┘   └─────┘ 
 30    iseqv := ⟨λ f i, rfl, λ f g H i, (H i).symm,
id                    └─┘            └──┘
src                     └─┘                  └──┘
typ                   └─┘            └──┘
 31      λ f g h H1 H2 i, (H1 i).trans (H2 i)⟩ }
id            └┘ └┘    └┘  └───┘   └┘ 
src                             └───┘
typ           └┘ └┘    └┘  └───┘   └┘ 
 32  
 33  end dfinsupp
 34  
 35  variable {ι}
 36  @[reducible] def dfinsupp [Π i, has_zero (β i)] : Type* :=
id                                  └──────┘   
src                                  └──────┘
typ                                 └──────┘   
doc    └───────┘
 37  quotient (dfinsupp.setoid ι β)
id   └──────┘  └─────────────┘  
src  └──────┘  └─────────────┘
typ  └──────┘  └─────────────┘  
 38  variable {β}
 39  
 40  notation `Π₀` binders `, ` r:(scoped f, dfinsupp f) := r
id                                           └──────┘
src                                          └──────┘
typ                                          └──────┘
 41  infix ` →ₚ `:25 := dfinsupp
id                      └──────┘
src                     └──────┘
typ                     └──────┘
 42  
 43  namespace dfinsupp
 44  
 45  section basic
 46  variables [Π i, has_zero (β i)]
id                  └──────┘    
src                  └──────┘
typ                 └──────┘    
 47  variables {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
id             
typ            
 48  variables [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]
id                  └──────┘             └──────┘     
src                  └──────┘               └──────┘
typ                 └──────┘             └──────┘     
 49  
 50  instance : has_coe_to_fun (Π₀ i, β i) :=
id              └────────────┘  └┘   
src             └────────────┘  └┘  
typ             └────────────┘  └┘   
 51  ⟨λ _, Π i, β i, λ f, quotient.lift_on f pre.to_fun $ λ _ _, funext⟩
id                   └──────────────┘  └────────┘        └────┘
src                       └──────────────┘   └────────┘          └────┘
typ                  └──────────────┘  └────────┘        └────┘
 52  
 53  instance : has_zero (Π₀ i, β i) := ⟨⟦⟨λ i, 0, ∅, λ i, or.inr rfl⟩⟧⟩
id              └──────┘  └┘                       └────┘ └─┘ 
src             └──────┘  └┘                            └────┘ └─┘ 
typ             └──────┘  └┘                       └────┘ └─┘ 
 54  instance : inhabited (Π₀ i, β i) := ⟨0⟩
id              └───────┘  └┘   
src             └───────┘  └┘  
typ             └───────┘  └┘   
 55  
 56  @[simp] lemma zero_apply {i : ι} : (0 : Π₀ i, β i) i = 0 := rfl
id                                          └┘            └─┘
src                                          └┘                └─┘
typ                                         └┘            └─┘
doc    └──┘
 57  
 58  @[ext]
doc    └─┘
 59  lemma ext {f g : Π₀ i, β i} (H : ∀ i, f i = g i) : f = g :=
id                    └┘                        
src                   └┘                                
typ                   └┘                        
 60  quotient.induction_on₂ f g (λ _ _ H, quotient.sound H) H
id   └────────────────────┘          └────────────┘   
src  └────────────────────┘               └────────────┘
typ  └────────────────────┘          └────────────┘   
 61  
 62  /-- The composition of `f : β₁ → β₂` and `g : Π₀ i, β₁ i` is
 63    `map_range f hf g : Π₀ i, β₂ i`, well defined when `f 0 = 0`. -/
 64  def map_range (f : Π i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (g : Π₀ i, β₁ i) : Π₀ i, β₂ i :=
id                          └┘    └┘                          └┘  └┘     └┘  └┘ 
src                                                                 └┘           └┘  
typ                         └┘    └┘                          └┘  └┘     └┘  └┘ 
 65  quotient.lift_on g (λ x, ⟦(⟨λ i, f i (x.1 i), x.2,
id   └──────────────┘                     
src  └──────────────┘                             
typ  └──────────────┘                     
 66    λ i, or.cases_on (x.3 i) or.inl $ λ H, or.inr $ by rw [H, hf]⟩ : pre ι β₂)⟧) $ λ x y H,
id         └─────────┘      └────┘       └────┘            └┘     └─┘  └┘         
src         └─────────┘        └────┘        └────┘      └──┘ └┘      └─┘      
typ        └─────────┘      └────┘       └────┘      └──┘└┘└┘    └─┘  └┘         
doc                                                       └──┘ └┘  
txt                                                       └──┘ └┘  
par                                                       └──┘ └┘  
pid                                                         └┘ └┘  
st                                                       └────┘└──┘
 67  quotient.sound $ λ i, by simp only [H i]
id   └────────────┘                      
src  └────────────┘           └─────────┘  └─
typ  └────────────┘          └─────────┘└─
doc                           └─────────┘  └─
txt                           └─────────┘  └─
par                           └─────────┘  └─
pid                               └──┘└┘  
st                           └────────────────
 68  
src  
typ  
doc  
txt  
par  
pid  
st   
 69  @[simp] lemma map_range_apply
doc    └──┘
 70    {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} {i : ι} :
id              └┘    └┘                          └┘  └┘        
src                                                     └┘  
typ             └┘    └┘                          └┘  └┘        
 71    map_range f hf g i = f i (g i) :=
id     └───────┘  └┘        
src    └───────┘          
typ    └───────┘  └┘        
doc    └───────┘
 72  quotient.induction_on g $ λ x, rfl
id   └───────────────────┘        └─┘
src  └───────────────────┘          └─┘
typ  └───────────────────┘        └─┘
 73  
 74  def zip_with (f : Π i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0) (g₁ : Π₀ i, β₁ i) (g₂ : Π₀ i, β₂ i) : (Π₀ i, β i) :=
id                         └┘    └┘                                 └┘  └┘         └┘  └┘      └┘   
src                                                                         └┘               └┘            └┘  
typ                        └┘    └┘                                 └┘  └┘         └┘  └┘      └┘   
 75  begin
st   └─────
 76    refine quotient.lift_on₂ g₁ g₂ (λ x y, ⟦(⟨λ i, f i (x.1 i) (y.1 i), x.2 + y.2,
id            └───────────────┘ └┘ └┘                                        
src    └─────┘└───────────────┘      └────┘   └──┘    └─┘ └┘  └─┘ └─┘ └─┘ └───
typ    └─────┘└───────────────┘└┘└┘  └────┘   └──┘   └─┘ └┘  └─┘ └─┘ └─┘ └───
doc    └─────┘                       └────┘    └──┘    └─┘ └┘  └─┘ └─┘ └─┘  └───
txt    └─────┘                       └────┘    └──┘    └─┘ └┘  └─┘ └─┘ └─┘  └───
par    └─────┘                       └────┘    └──┘    └─┘ └┘  └─┘ └─┘ └─┘  └───
pid                                 └────┘    └──┘    └─┘ └┘  └─┘ └─┘ └─┘  └───
st   ─────────────────────────────────────────────────────────────────────────────────
 77      λ i, _⟩ : pre ι β)⟧) _,
id                 └─┘   
src  ───┘ └───────┘└─┘  └─┘
typ  ───┘ └───────┘└─┘└─┘
doc  ───┘ └───────┘      └─┘
txt  ───┘ └───────┘      └─┘
par  ───┘ └───────┘      └─┘
pid  ───┘ └───────┘      └─┘
st   ─────────────────────────┘└─
 78    { cases x.3 i with h1 h1,
id                
src      └────┘ └─┘ └─────────┘
typ      └────┘└─┘└─────────┘
doc      └────┘ └─┘ └─────────┘
txt      └────┘ └─┘ └─────────┘
par      └────┘ └─┘ └─────────┘
pid            └─┘ └─────────┘
st   ───┘└────────────────────┘└─
 79      { left, rw multiset.mem_add, left, exact h1 },
id                  └──────────────┘              └┘
src        └──┘  └─┘└──────────────┘  └──┘  └────┘  
typ        └──┘  └─┘└──────────────┘  └──┘  └────┘└┘
doc        └──┘  └─┘                  └──┘  └────┘  
txt        └──┘  └─┘                  └──┘  └────┘  
par        └──┘  └─┘                  └──┘  └────┘  
pid                                               
st   ─────┘└──┘└───────────────────┘└────┘└─────────┘└┘
 80      cases y.3 i with h2 h2,
id                
src      └────┘ └─┘ └─────────┘
typ      └────┘└─┘└─────────┘
doc      └────┘ └─┘ └─────────┘
txt      └────┘ └─┘ └─────────┘
par      └────┘ └─┘ └─────────┘
pid            └─┘ └─────────┘
st   ─────────────────────────┘└─
 81      { left, rw multiset.mem_add, right, exact h2 },
id                  └──────────────┘               └┘
src        └──┘  └─┘└──────────────┘  └───┘  └────┘  
typ        └──┘  └─┘└──────────────┘  └───┘  └────┘└┘
doc        └──┘  └─┘                  └───┘  └────┘  
txt        └──┘  └─┘                  └───┘  └────┘  
par        └──┘  └─┘                  └───┘  └────┘  
pid                                                
st   ─────┘└──┘└───────────────────┘└─────┘└─────────┘└┘
 82      right, rw [h1, h2, hf] },
id                  └┘  └┘  └┘
src      └───┘  └──┘  └┘  └┘  └┘
typ      └───┘  └──┘└┘└┘└┘└┘└┘└┘
doc      └───┘  └──┘  └┘  └┘  └┘
txt      └───┘  └──┘  └┘  └┘  └┘
par      └───┘  └──┘  └┘  └┘  └┘
pid               └┘  └┘  └┘  
st   ────────┘└──────┘└──┘└──┘└┘
 83    exact λ x₁ x₂ y₁ y₂ H1 H2, quotient.sound $ λ i, by simp only [H1 i, H2 i]
id                                └────────────┘                      └┘   └┘ 
src    └────┘ └──────────────────┘└────────────┘  └──┘  └─────────┘   └┘   └┘
typ    └────┘ └──────────────────┘└────────────┘  └──┘  └─────────┘└┘└┘└┘└┘
doc    └────┘ └──────────────────┘                └──┘  └─────────┘   └┘   └┘
txt    └────┘ └──────────────────┘                └──┘  └─────────┘   └┘   └┘
par    └────┘ └──────────────────┘                └──┘  └─────────┘   └┘   └┘
pid          └──────────────────┘                └──┘  └──────────┘   └┘   └┘
st   ────────────────────────────────────────────────────┘└──────────────────────┘
 84  end
st   └─┘
 85  
 86  @[simp] lemma zip_with_apply
doc    └──┘
 87    {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} {i : ι} :
id              └┘    └┘                                 └┘  └┘         └┘  └┘        
src                                                              └┘               └┘  
typ             └┘    └┘                                 └┘  └┘         └┘  └┘        
 88    zip_with f hf g₁ g₂ i = f i (g₁ i) (g₂ i) :=
id     └──────┘  └┘ └┘ └┘      └┘    └┘ 
src    └──────┘              
typ    └──────┘  └┘ └┘ └┘      └┘    └┘ 
 89  quotient.induction_on₂ g₁ g₂ $ λ _ _, rfl
id   └────────────────────┘ └┘ └┘        └─┘
src  └────────────────────┘                └─┘
typ  └────────────────────┘ └┘ └┘        └─┘
 90  
 91  end basic
 92  
 93  section algebra
 94  
 95  instance [Π i, add_monoid (β i)] : has_add (Π₀ i, β i) :=
id                 └────────┘        └─────┘  └┘   
src                 └────────┘          └─────┘  └┘  
typ                └────────┘        └─────┘  └┘   
 96  ⟨zip_with (λ _, (+)) (λ _, add_zero 0)⟩
id    └──────┘               └──────┘
src   └──────┘                 └──────┘
typ   └──────┘               └──────┘
 97  
 98  @[simp] lemma add_apply [Π i, add_monoid (β i)] {g₁ g₂ : Π₀ i, β i} {i : ι} :
id                                └────────┘               └┘          
src                                └────────┘                 └┘  
typ                               └────────┘               └┘          
doc    └──┘
 99    (g₁ + g₂) i = g₁ i + g₂ i :=
id      └┘  └┘    └┘   └┘ 
src                     
typ     └┘  └┘    └┘   └┘ 
100  zip_with_apply
id   └────────────┘
src  └────────────┘
typ  └────────────┘
101  
102  instance [Π i, add_monoid (β i)] : add_monoid (Π₀ i, β i) :=
id                 └────────┘        └────────┘  └┘   
src                 └────────┘          └────────┘  └┘  
typ                └────────┘        └────────┘  └┘   
103  { add_monoid .
104    zero      := 0,
105    add       := (+),
id                  
src                 
typ                 
st                  
106    add_assoc := λ f g h, ext $ λ i, by simp only [add_apply, add_assoc],
id                        └─┘                     └───────┘  └───────┘
src                          └─┘           └─────────┘└───────┘└┘└───────┘
typ                       └─┘          └─────────┘└───────┘└┘└───────┘
doc                                        └─────────┘         └┘         
txt                                        └─────────┘         └┘         
par                                        └─────────┘         └┘         
pid                                            └──┘└┘         └┘         
st                                        └───────────────────────────────┘
107    zero_add  := λ f, ext $ λ i, by simp only [add_apply, zero_apply, zero_add],
id                      └─┘                     └───────┘  └────────┘  └──────┘
src                      └─┘           └─────────┘└───────┘└┘└────────┘└┘└──────┘
typ                     └─┘          └─────────┘└───────┘└┘└────────┘└┘└──────┘
doc                                    └─────────┘         └┘          └┘        
txt                                    └─────────┘         └┘          └┘        
par                                    └─────────┘         └┘          └┘        
pid                                        └──┘└┘         └┘          └┘        
st                                    └──────────────────────────────────────────┘
108    add_zero  := λ f, ext $ λ i, by simp only [add_apply, zero_apply, add_zero] }
id                      └─┘                     └───────┘  └────────┘  └──────┘
src                      └─┘           └─────────┘└───────┘└┘└────────┘└┘└──────┘└┘
typ                     └─┘          └─────────┘└───────┘└┘└────────┘└┘└──────┘└┘
doc                                    └─────────┘         └┘          └┘        └┘
txt                                    └─────────┘         └┘          └┘        └┘
par                                    └─────────┘         └┘          └┘        └┘
pid                                        └──┘└┘         └┘          └┘        
st                                    └───────────────────────────────────────────┘
109  
110  instance [Π i, add_monoid (β i)] {i : ι} : is_add_monoid_hom (λ g : Π₀ i : ι, β i, g i) :=
id                 └────────┘               └───────────────┘        └┘          
src                 └────────┘                  └───────────────┘        └┘      
typ                └────────┘               └───────────────┘        └┘          
doc                                             └───────────────┘
111  { map_add := λ _ _, add_apply, map_zero := zero_apply }
id                     └───────┘              └────────┘
src                      └───────┘              └────────┘
typ                    └───────┘              └────────┘
112  
113  instance [Π i, add_group (β i)] : has_neg (Π₀ i, β i) :=
id                 └───────┘        └─────┘  └┘   
src                 └───────┘          └─────┘  └┘  
typ                └───────┘        └─────┘  └┘   
114  ⟨λ f, f.map_range (λ _, has_neg.neg) (λ _, neg_zero)⟩
id        └────────┘      └─────────┘       └──────┘
src         └────────┘       └─────────┘        └──────┘
typ       └────────┘      └─────────┘       └──────┘
doc         └────────┘
115  
116  instance [Π i, add_comm_monoid (β i)] : add_comm_monoid (Π₀ i, β i) :=
id                 └─────────────┘        └─────────────┘  └┘   
src                 └─────────────┘          └─────────────┘  └┘  
typ                └─────────────┘        └─────────────┘  └┘   
117  { add_comm := λ f g, ext $ λ i, by simp only [add_apply, add_comm],
id                      └─┘                     └───────┘  └──────┘
src                       └─┘           └─────────┘└───────┘└┘└──────┘
typ                     └─┘          └─────────┘└───────┘└┘└──────┘
doc                                     └─────────┘         └┘        
txt                                     └─────────┘         └┘        
par                                     └─────────┘         └┘        
pid                                         └──┘└┘         └┘        
st                                     └──────────────────────────────┘
118    .. dfinsupp.add_monoid }
id        └─────────────────┘
src       └─────────────────┘
typ       └─────────────────┘
119  
120  @[simp] lemma neg_apply [Π i, add_group (β i)] {g : Π₀ i, β i} {i : ι} : (- g) i = - g i :=
id                                └───────┘           └┘                      
src                                └───────┘             └┘                          
typ                               └───────┘           └┘                      
doc    └──┘
121  map_range_apply
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
122  
123  instance [Π i, add_group (β i)] : add_group (Π₀ i, β i) :=
id                 └───────┘        └───────┘  └┘   
src                 └───────┘          └───────┘  └┘  
typ                └───────┘        └───────┘  └┘   
124  { add_left_neg := λ f, ext $ λ i, by simp only [add_apply, neg_apply, zero_apply, add_left_neg],
id                         └─┘                     └───────┘  └───────┘  └────────┘  └──────────┘
src                         └─┘           └─────────┘└───────┘└┘└───────┘└┘└────────┘└┘└──────────┘
typ                        └─┘          └─────────┘└───────┘└┘└───────┘└┘└────────┘└┘└──────────┘
doc                                       └─────────┘         └┘         └┘          └┘            
txt                                       └─────────┘         └┘         └┘          └┘            
par                                       └─────────┘         └┘         └┘          └┘            
pid                                           └──┘└┘         └┘         └┘          └┘            
st                                       └─────────────────────────────────────────────────────────┘
125    .. dfinsupp.add_monoid,
id        └─────────────────┘
src       └─────────────────┘
typ       └─────────────────┘
126    .. (infer_instance : has_neg (Π₀ i, β i)) }
id         └────────────┘   └─────┘  └┘   
src        └────────────┘   └─────┘  └┘  
typ        └────────────┘   └─────┘  └┘   
doc        └────────────┘
127  
128  @[simp] lemma sub_apply [Π i, add_group (β i)] {g₁ g₂ : Π₀ i, β i} {i : ι} : (g₁ - g₂) i = g₁ i - g₂ i :=
id                                └───────┘               └┘               └┘  └┘    └┘   └┘ 
src                                └───────┘                 └┘                                   
typ                               └───────┘               └┘               └┘  └┘    └┘   └┘ 
doc    └──┘
129  by rw [sub_eq_add_neg]; simp
id          └────────────┘
src     └──┘└────────────┘  └────
typ     └──┘└────────────┘  └────
doc     └──┘                └────
txt     └──┘                └────
par     └──┘                └────
pid       └┘                    
st     └─────────────────┘└──────
130  
src  
typ  
doc  
txt  
par  
pid  
st   
131  instance [Π i, add_comm_group (β i)] : add_comm_group (Π₀ i, β i) :=
id                 └────────────┘        └────────────┘  └┘   
src                 └────────────┘          └────────────┘  └┘  
typ                └────────────┘        └────────────┘  └┘   
132  { add_comm := λ f g, ext $ λ i, by simp only [add_apply, add_comm],
id                      └─┘                     └───────┘  └──────┘
src                       └─┘           └─────────┘└───────┘└┘└──────┘
typ                     └─┘          └─────────┘└───────┘└┘└──────┘
doc                                     └─────────┘         └┘        
txt                                     └─────────┘         └┘        
par                                     └─────────┘         └┘        
pid                                         └──┘└┘         └┘        
st                                     └──────────────────────────────┘
133    ..dfinsupp.add_group }
id       └────────────────┘
src      └────────────────┘
typ      └────────────────┘
134  
135  def to_has_scalar {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] : has_scalar γ (Π₀ i, β i) :=
id                                   └──┘        └────────────┘           └────┘         └────────┘   └┘   
src                                  └──┘          └────────────┘              └────┘            └────────┘    └┘  
typ                                  └──┘        └────────────┘           └────┘         └────────┘   └┘   
doc                                                                            └────┘            └────────┘
136  ⟨λc v, v.map_range (λ _, (•) c) (λ _, smul_zero _)⟩
id        └────────┘                └───────┘
src          └────────┘                   └───────┘
typ       └────────┘                └───────┘
doc          └────────┘
137  local attribute [instance] to_has_scalar
id                              └───────────┘
src                             └───────────┘
typ                             └───────────┘
138  
139  @[simp] lemma smul_apply {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] {i : ι} {b : γ} {v : Π₀ i, β i} :
id                                          └──┘        └────────────┘           └────┘                          └┘   
src                                         └──┘          └────────────┘              └────┘                               └┘  
typ                                         └──┘        └────────────┘           └────┘                          └┘   
doc    └──┘                                                                           └────┘
140    (b • v) i = b • (v i) :=
id                
src                
typ               
141  map_range_apply
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
142  
143  def to_module {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] : module γ (Π₀ i, β i) :=
id                               └──┘        └────────────┘           └────┘         └────┘   └┘   
src                              └──┘          └────────────┘              └────┘            └────┘    └┘  
typ                              └──┘        └────────────┘           └────┘         └────┘   └┘   
doc                                                                        └────┘            └────┘
144  module.of_core {
id   └────────────┘
src  └────────────┘
typ  └────────────┘
145    smul_add := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, smul_add],
id                       └─┘                     └───────┘  └────────┘  └──────┘
src                         └─┘           └─────────┘└───────┘└┘└────────┘└┘└──────┘
typ                      └─┘          └─────────┘└───────┘└┘└────────┘└┘└──────┘
doc                                       └─────────┘         └┘          └┘        
txt                                       └─────────┘         └┘          └┘        
par                                       └─────────┘         └┘          └┘        
pid                                           └──┘└┘         └┘          └┘        
st                                       └──────────────────────────────────────────┘
146    add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul],
id                       └─┘                     └───────┘  └────────┘  └──────┘
src                         └─┘           └─────────┘└───────┘└┘└────────┘└┘└──────┘
typ                      └─┘          └─────────┘└───────┘└┘└────────┘└┘└──────┘
doc                                       └─────────┘         └┘          └┘        
txt                                       └─────────┘         └┘          └┘        
par                                       └─────────┘         └┘          └┘        
pid                                           └──┘└┘         └┘          └┘        
st                                       └──────────────────────────────────────────┘
147    one_smul := λ x, ext $ λ i, by simp only [smul_apply, one_smul],
id                     └─┘                     └────────┘  └──────┘
src                     └─┘           └─────────┘└────────┘└┘└──────┘
typ                    └─┘          └─────────┘└────────┘└┘└──────┘
doc                                   └─────────┘          └┘        
txt                                   └─────────┘          └┘        
par                                   └─────────┘          └┘        
pid                                       └──┘└┘          └┘        
st                                   └───────────────────────────────┘
148    mul_smul := λ r s x, ext $ λ i, by simp only [smul_apply, smul_smul],
id                       └─┘                     └────────┘  └───────┘
src                         └─┘           └─────────┘└────────┘└┘└───────┘
typ                      └─┘          └─────────┘└────────┘└┘└───────┘
doc                                       └─────────┘          └┘         
txt                                       └─────────┘          └┘         
par                                       └─────────┘          └┘         
pid                                           └──┘└┘          └┘         
st                                       └────────────────────────────────┘
149    .. (infer_instance : has_scalar γ (Π₀ i, β i)) }
id         └────────────┘   └────────┘   └┘   
src        └────────────┘   └────────┘    └┘  
typ        └────────────┘   └────────┘   └┘   
doc        └────────────┘   └────────┘
150  
151  end algebra
152  
153  section filter_and_subtype_domain
154  
155  /-- `filter p f` is the function which is `f i` if `p i` is true and 0 otherwise. -/
156  def filter [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p] (f : Π₀ i, β i) : Π₀ i, β i :=
id                   └──────┘                     └────────────┘        └┘       └┘   
src                   └──────┘                        └────────────┘         └┘          └┘  
typ                  └──────┘                     └────────────┘        └┘       └┘   
157  quotient.lift_on f (λ x, ⟦(⟨λ i, if p i then x.1 i else 0, x.2,
id   └──────────────┘                                  
src  └──────────────┘                                          
typ  └──────────────┘                                  
158    λ i, or.cases_on (x.3 i) or.inl $ λ H, or.inr $ by rw [H, if_t_t]⟩ : pre ι β)⟧) $ λ x y H,
id         └─────────┘      └────┘       └────┘            └────┘     └─┘           
src         └─────────┘        └────┘        └────┘      └──┘ └┘└────┘    └─┘     
typ        └─────────┘      └────┘       └────┘      └──┘└┘└────┘    └─┘           
doc                                                       └──┘ └┘      
txt                                                       └──┘ └┘      
par                                                       └──┘ └┘      
pid                                                         └┘ └┘      
st                                                       └────┘└──────┘
159  quotient.sound $ λ i, by simp only [H i]
id   └────────────┘                      
src  └────────────┘           └─────────┘  └─
typ  └────────────┘          └─────────┘└─
doc                           └─────────┘  └─
txt                           └─────────┘  └─
par                           └─────────┘  └─
pid                               └──┘└┘  
st                           └────────────────
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161  @[simp] lemma filter_apply [Π i, has_zero (β i)]
id                                   └──────┘   
src                                   └──────┘
typ                                  └──────┘   
doc    └──┘
162    {p : ι → Prop} [decidable_pred p] {i : ι} {f : Π₀ i, β i} :
id                    └────────────┘               └┘   
src                    └────────────┘                 └┘  
typ                   └────────────┘               └┘   
163    f.filter p i = if p i then f i else 0 :=
id     └─────┘               
src     └─────┘     
typ    └─────┘               
doc     └─────┘
164  quotient.induction_on f $ λ x, rfl
id   └───────────────────┘        └─┘
src  └───────────────────┘          └─┘
typ  └───────────────────┘        └─┘
165  
166  @[simp] lemma filter_apply_pos [Π i, has_zero (β i)]
id                                       └──────┘   
src                                       └──────┘
typ                                      └──────┘   
doc    └──┘
167    {p : ι → Prop} [decidable_pred p] {f : Π₀ i, β i} {i : ι} (h : p i) :
id                    └────────────┘        └┘                  
src                    └────────────┘         └┘  
typ                   └────────────┘        └┘                  
168    f.filter p i = f i :=
id     └─────┘     
src     └─────┘     
typ    └─────┘     
doc     └─────┘
169  by simp only [filter_apply, if_pos h]
id                 └──────────┘  └────┘ 
src     └─────────┘└──────────┘└┘└────┘ └─
typ     └─────────┘└──────────┘└┘└────┘└─
doc     └─────────┘            └┘       └─
txt     └─────────┘            └┘       └─
par     └─────────┘            └┘       └─
pid         └──┘└┘            └┘       
st     └───────────────────────────────────
170  
src  
typ  
doc  
txt  
par  
pid  
st   
171  @[simp] lemma filter_apply_neg [Π i, has_zero (β i)]
id                                       └──────┘   
src                                       └──────┘
typ                                      └──────┘   
doc    └──┘
172    {p : ι → Prop} [decidable_pred p] {f : Π₀ i, β i} {i : ι} (h : ¬ p i) :
id                    └────────────┘        └┘                   
src                    └────────────┘         └┘                     
typ                   └────────────┘        └┘                   
173    f.filter p i = 0 :=
id     └─────┘   
src     └─────┘     
typ    └─────┘   
doc     └─────┘
174  by simp only [filter_apply, if_neg h]
id                 └──────────┘  └────┘ 
src     └─────────┘└──────────┘└┘└────┘ └─
typ     └─────────┘└──────────┘└┘└────┘└─
doc     └─────────┘            └┘       └─
txt     └─────────┘            └┘       └─
par     └─────────┘            └┘       └─
pid         └──┘└┘            └┘       
st     └───────────────────────────────────
175  
src  
typ  
doc  
txt  
par  
pid  
st   
176  lemma filter_pos_add_filter_neg [Π i, add_monoid (β i)] {f : Π₀ i, β i}
id                                        └────────┘           └┘   
src                                        └────────┘             └┘  
typ                                       └────────┘           └┘   
177    {p : ι → Prop} [decidable_pred p] :
id                    └────────────┘ 
src                    └────────────┘
typ                   └────────────┘ 
178    f.filter p + f.filter (λi, ¬ p i) = f :=
id     └─────┘   └─────┘          
src     └─────┘     └─────┘            
typ    └─────┘   └─────┘          
doc     └─────┘      └─────┘
179  ext $ λ i, by simp only [add_apply, filter_apply]; split_ifs; simp only [add_zero, zero_add]
id   └─┘                     └───────┘  └──────────┘                         └──────┘  └──────┘
src  └─┘           └─────────┘└───────┘└┘└──────────┘  └───────┘  └─────────┘└──────┘└┘└──────┘└─
typ  └─┘          └─────────┘└───────┘└┘└──────────┘  └───────┘  └─────────┘└──────┘└┘└──────┘└─
doc                └─────────┘         └┘              └───────┘  └─────────┘        └┘        └─
txt                └─────────┘         └┘              └───────┘  └─────────┘        └┘        └─
par                └─────────┘         └┘              └───────┘  └─────────┘        └┘        └─
pid                    └──┘└┘         └┘                             └──┘└┘        └┘        
st                └───────────────────────────────────────────────────────────────────────────────
180  
src  
typ  
doc  
txt  
par  
pid  
st   
181  /-- `subtype_domain p f` is the restriction of the finitely supported function
182    `f` to the subtype `p`. -/
183  def subtype_domain [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p]
id                           └──────┘                     └────────────┘ 
src                           └──────┘                        └────────────┘
typ                          └──────┘                     └────────────┘ 
184    (f : Π₀ i, β i) : Π₀ i : subtype p, β i.1 :=
id          └┘       └┘     └─────┘   
src         └┘          └┘     └─────┘      
typ         └┘       └┘     └─────┘   
185  begin
st   └─────
186    fapply quotient.lift_on f,
id            └──────────────┘ 
src    └─────┘└──────────────┘
typ    └─────┘└──────────────┘
doc    └─────┘                
txt    └─────┘                
par    └─────┘                
pid                          
st   ──────────────────────────┘└─
187    { intro x, refine ⟦⟨λ i, x.1 i.1, (x.2.filter p).attach.map $ λ j, ⟨j.1, (multiset.mem_filter.1 j.2).2⟩, _⟩⟧,
id                                                                            └─────────────────┘              
src      └─────┘  └─────┘  └──┘ └─┘ └──┘  └────────┘ └───────────┘  └──┘  └──┘ └─────────────────┘└─┘ └────────┘
typ      └─────┘  └─────┘  └──┘ └─┘ └──┘ └────────┘└───────────┘  └──┘  └──┘ └─────────────────┘└─┘ └────────┘
doc      └─────┘  └─────┘   └──┘ └─┘ └──┘  └────────┘ └───────────┘  └──┘  └──┘                    └─┘ └────────┘
txt      └─────┘  └─────┘   └──┘ └─┘ └──┘  └────────┘ └───────────┘  └──┘  └──┘                    └─┘ └────────┘
par      └─────┘  └─────┘   └──┘ └─┘ └──┘  └────────┘ └───────────┘  └──┘  └──┘                    └─┘ └────────┘
pid           └┘           └──┘ └─┘ └──┘  └────────┘ └───────────┘  └──┘  └──┘                    └─┘ └────────┘
st   ───┘└─────┘└─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
188      refine λ i, or.cases_on (x.3 i.1) (λ H, _) or.inr,
id                   └─────────┘                   └────┘
src      └─────┘ └──┘└─────────┘  └─┘ └──┘  └─────┘└────┘
typ      └─────┘ └──┘└─────────┘ └─┘ └──┘  └─────┘└────┘
doc      └─────┘ └──┘             └─┘ └──┘  └─────┘
txt      └─────┘ └──┘             └─┘ └──┘  └─────┘
par      └─────┘ └──┘             └─┘ └──┘  └─────┘
pid             └──┘             └─┘ └──┘  └─────┘
st   ────────────────────────────────────────────────────┘└─
189      left, rw multiset.mem_map, refine ⟨⟨i.1, multiset.mem_filter.2 ⟨H, i.2⟩⟩, _, subtype.eta _ _⟩,
id                └──────────────┘                └─────────────────┘               └─────────┘
src      └──┘  └─┘└──────────────┘  └─────┘   └──┘└─────────────────┘└─┘  └┘ └───────┘└─────────┘└───┘
typ      └──┘  └─┘└──────────────┘  └─────┘   └──┘└─────────────────┘└─┘ └┘└───────┘└─────────┘└───┘
doc      └──┘  └─┘                  └─────┘   └──┘                   └─┘  └┘ └───────┘           └───┘
txt      └──┘  └─┘                  └─────┘   └──┘                   └─┘  └┘ └───────┘           └───┘
par      └──┘  └─┘                  └─────┘   └──┘                   └─┘  └┘ └───────┘           └───┘
pid                                         └──┘                   └─┘  └┘ └───────┘           └───┘
st   ───────┘└───────────────────┘└──────────────────────────────────────────────────────────────────┘└─
190      apply multiset.mem_attach },
id             └─────────────────┘
src      └────┘└─────────────────┘
typ      └────┘└─────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ─────────────────────────────┘└┘
191    intros x y H,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
192    exact quotient.sound (λ i, H i.1)
id           └────────────┘       
src    └────┘└────────────┘  └──┘  └──┘
typ    └────┘└────────────┘  └──┘ └──┘
doc    └────┘                └──┘  └──┘
txt    └────┘                └──┘  └──┘
par    └────┘                └──┘  └──┘
pid                         └──┘  └─┘
st   ───────────────────────────────────┘
193  end
st   └─┘
194  
195  @[simp] lemma subtype_domain_zero [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p] :
id                                          └──────┘                     └────────────┘ 
src                                          └──────┘                        └────────────┘
typ                                         └──────┘                     └────────────┘ 
doc    └──┘
196    subtype_domain p (0 : Π₀ i, β i) = 0 :=
id     └────────────┘       └┘     
src    └────────────┘        └┘        
typ    └────────────┘       └┘     
doc    └────────────┘
197  rfl
id   └─┘
src  └─┘
typ  └─┘
198  
199  @[simp] lemma subtype_domain_apply [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p]
id                                           └──────┘                     └────────────┘ 
src                                           └──────┘                        └────────────┘
typ                                          └──────┘                     └────────────┘ 
doc    └──┘
200    {i : subtype p} {v : Π₀ i, β i} :
id          └─────┘        └┘   
src         └─────┘         └┘  
typ         └─────┘        └┘   
201    (subtype_domain p v) i = v (i.val) :=
id      └────────────┘        └──┘
src     └────────────┘             └──┘
typ     └────────────┘        └──┘
doc     └────────────┘
202  quotient.induction_on v $ λ x, rfl
id   └───────────────────┘        └─┘
src  └───────────────────┘          └─┘
typ  └───────────────────┘        └─┘
203  
204  @[simp] lemma subtype_domain_add [Π i, add_monoid (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ i, β i} :
id                                         └────────┘                     └────────────┘           └┘   
src                                         └────────┘                        └────────────┘            └┘  
typ                                        └────────┘                     └────────────┘           └┘   
doc    └──┘
205    (v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=
id        └┘ └────────────┘    └─────────────┘   └┘└─────────────┘ 
src           └────────────┘      └─────────────┘      └─────────────┘
typ       └┘ └────────────┘    └─────────────┘   └┘└─────────────┘ 
doc            └────────────┘       └─────────────┘       └─────────────┘
206  ext $ λ i, by simp only [add_apply, subtype_domain_apply]
id   └─┘                     └───────┘  └──────────────────┘
src  └─┘           └─────────┘└───────┘└┘└──────────────────┘└─
typ  └─┘          └─────────┘└───────┘└┘└──────────────────┘└─
doc                └─────────┘         └┘                    └─
txt                └─────────┘         └┘                    └─
par                └─────────┘         └┘                    └─
pid                    └──┘└┘         └┘                    
st                └────────────────────────────────────────────
207  
src  
typ  
doc  
txt  
par  
pid  
st   
208  instance subtype_domain.is_add_monoid_hom [Π i, add_monoid (β i)] {p : ι → Prop} [decidable_pred p] :
id                                                  └────────┘                     └────────────┘ 
src                                                  └────────┘                        └────────────┘
typ                                                 └────────┘                     └────────────┘ 
209    is_add_monoid_hom (subtype_domain p : (Π₀ i : ι, β i) → Π₀ i : subtype p, β i) :=
id     └───────────────┘  └────────────┘     └┘           └┘     └─────┘   
src    └───────────────┘  └────────────┘      └┘              └┘     └─────┘  
typ    └───────────────┘  └────────────┘     └┘           └┘     └─────┘   
doc    └───────────────┘  └────────────┘
210  { map_add := λ _ _, subtype_domain_add, map_zero := subtype_domain_zero }
id                     └────────────────┘              └─────────────────┘
src                      └────────────────┘              └─────────────────┘
typ                    └────────────────┘              └─────────────────┘
211  
212  @[simp] lemma subtype_domain_neg [Π i, add_group (β i)] {p : ι → Prop} [decidable_pred p] {v : Π₀ i, β i} :
id                                         └───────┘                     └────────────┘        └┘   
src                                         └───────┘                        └────────────┘         └┘  
typ                                        └───────┘                     └────────────┘        └┘   
doc    └──┘
213    (- v).subtype_domain p = - v.subtype_domain p :=
id        └────────────┘     └─────────────┘ 
src        └────────────┘       └─────────────┘
typ       └────────────┘     └─────────────┘ 
doc         └────────────┘         └─────────────┘
214  ext $ λ i, by simp only [neg_apply, subtype_domain_apply]
id   └─┘                     └───────┘  └──────────────────┘
src  └─┘           └─────────┘└───────┘└┘└──────────────────┘└─
typ  └─┘          └─────────┘└───────┘└┘└──────────────────┘└─
doc                └─────────┘         └┘                    └─
txt                └─────────┘         └┘                    └─
par                └─────────┘         └┘                    └─
pid                    └──┘└┘         └┘                    
st                └────────────────────────────────────────────
215  
src  
typ  
doc  
txt  
par  
pid  
st   
216  @[simp] lemma subtype_domain_sub [Π i, add_group (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ i, β i} :
id                                         └───────┘                     └────────────┘           └┘   
src                                         └───────┘                        └────────────┘            └┘  
typ                                        └───────┘                     └────────────┘           └┘   
doc    └──┘
217    (v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=
id        └┘ └────────────┘    └─────────────┘   └┘└─────────────┘ 
src           └────────────┘      └─────────────┘      └─────────────┘
typ       └┘ └────────────┘    └─────────────┘   └┘└─────────────┘ 
doc            └────────────┘       └─────────────┘       └─────────────┘
218  ext $ λ i, by simp only [sub_apply, subtype_domain_apply]
id   └─┘                     └───────┘  └──────────────────┘
src  └─┘           └─────────┘└───────┘└┘└──────────────────┘└─
typ  └─┘          └─────────┘└───────┘└┘└──────────────────┘└─
doc                └─────────┘         └┘                    └─
txt                └─────────┘         └┘                    └─
par                └─────────┘         └┘                    └─
pid                    └──┘└┘         └┘                    
st                └────────────────────────────────────────────
219  
src  
typ  
doc  
txt  
par  
pid  
st   
220  end filter_and_subtype_domain
221  
222  
223  variable [decidable_eq ι]
id             └──────────┘
src            └──────────┘
typ            └──────────┘
224  
225  section basic
226  variable [Π i, has_zero (β i)]
id                 └──────┘    
src                 └──────┘
typ                └──────┘    
227  
228  lemma finite_supp (f : Π₀ i, β i) : set.finite {i | f i ≠ 0} :=
id                          └┘       └────────┘      
src                         └┘          └────────┘         
typ                         └┘       └────────┘      
doc                                      └────────┘
229  quotient.induction_on f $ λ x, set.finite_subset
id   └───────────────────┘        └───────────────┘
src  └───────────────────┘          └───────────────┘
typ  └───────────────────┘        └───────────────┘
230    (finset.finite_to_set x.2.to_finset) $ λ i H,
id      └──────────────────┘  └───────┘        
src     └──────────────────┘   └───────┘
typ     └──────────────────┘  └───────┘        
doc                             └───────┘
231  multiset.mem_to_finset.2 $ (x.3 i).resolve_right H
id   └────────────────────┘        └───────────┘  
src  └────────────────────┘          └───────────┘
typ  └────────────────────┘        └───────────┘  
232  
233  def mk (s : finset ι) (x : Π i : (↑s : set ι), β i.1) : Π₀ i, β i :=
id               └────┘                 └─┘          └┘   
src              └────┘                    └─┘             └┘  
typ              └────┘                 └─┘          └┘   
doc              └────┘
234  ⟦⟨λ i, if H : i ∈ s then x ⟨i, H⟩ else 0, s.1,
id        └┘                          
src        └┘                                
typ       └┘                          
235  λ i, if H : i ∈ s then or.inl H else or.inr $ dif_neg H⟩⟧
id       └┘             └────┘       └────┘  └─────┘  
src       └┘               └────┘        └────┘   └─────┘   
typ      └┘             └────┘       └────┘  └─────┘  
236  
237  @[simp] lemma mk_apply {s : finset ι} {x : Π i : (↑s : set ι), β i.1} {i : ι} :
id                               └────┘                 └─┘             
src                              └────┘                    └─┘        
typ                              └────┘                 └─┘             
doc    └──┘                      └────┘
238    (mk s x : Π i, β i) i = if H : i ∈ s then x ⟨i, H⟩ else 0 :=
id      └┘              └┘                        
src     └┘                    └┘       
typ     └┘              └┘                        
239  rfl
id   └─┘
src  └─┘
typ  └─┘
240  
241  theorem mk_inj (s : finset ι) : function.injective (@mk ι β _ _ s) :=
id                       └────┘     └────────────────┘   └┘       
src                      └────┘      └────────────────┘   └┘
typ                      └────┘     └────────────────┘   └┘       
doc                      └────┘
242  begin
st   └─────
243    intros x y H,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
244    ext i,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
245    have h1 : (mk s x : Π i, β i) i = (mk s y : Π i, β i) i, {rw H},
id                                      └┘                    
src    └────────┘     └─┘ └┘   └┘  └┘  └─┘ └┘   └┘    └─┘
typ    └────────┘    └─┘ └┘   └┘  └┘└─┘ └┘  └┘   └─┘
doc    └────────┘     └─┘ └┘   └┘       └─┘ └┘   └┘    └─┘
txt    └────────┘     └─┘ └┘   └┘       └─┘ └┘   └┘    └─┘
par    └────────┘     └─┘ └┘   └┘       └─┘ └┘   └┘    └─┘
pid    └─────┘└─┘     └─┘ └┘   └┘       └─┘ └┘   └┘      
st   ────────────────────────────────────────────────────────┘└────┘└┘
246    cases i with i hi,
id           
src    └────┘ └────────┘
typ    └────┘└────────┘
doc    └────┘ └────────┘
txt    └────┘ └────────┘
par    └────┘ └────────┘
pid          └────────┘
st   ──────────────────┘└─
247    change i ∈ s at hi,
id              
src    └─────┘  └────┘
typ    └─────┘└────┘
doc    └─────┘   └────┘
txt    └─────┘   └────┘
par    └─────┘   └────┘
pid             └───┘
st   ───────────────────┘└─
248    dsimp only [mk_apply, subtype.coe_mk] at h1,
id                 └──────┘  └────────────┘
src    └──────────┘└──────┘└┘└────────────┘└─────┘
typ    └──────────┘└──────┘└┘└────────────┘└─────┘
doc    └──────────┘        └┘              └─────┘
txt    └──────────┘        └┘              └─────┘
par    └──────────┘        └┘              └─────┘
pid         └───┘└┘        └┘              └───┘
st   ────────────────────────────────────────────┘└─
249    simpa only [dif_pos hi] using h1
id                 └─────┘ └┘        └┘
src    └──────────┘└─────┘  └──────┘  
typ    └──────────┘└─────┘└┘└──────┘└┘
doc    └──────────┘         └──────┘  
txt    └──────────┘         └──────┘  
par    └──────────┘         └──────┘  
pid         └──┘└┘         └────┘  
st   ──────────────────────────────────┘
250  end
st   └─┘
251  
252  def single (i : ι) (b : β i) : Π₀ i, β i :=
id                               └┘   
src                                 └┘  
typ                              └┘   
253  mk (finset.singleton i) $ λ j, eq.rec_on (finset.mem_singleton.1 j.2).symm b
id   └┘  └──────────────┘         └───────┘  └──────────────────┘    └──┘  
src  └┘  └──────────────┘           └───────┘  └──────────────────┘     └──┘
typ  └┘  └──────────────┘         └───────┘  └──────────────────┘    └──┘  
doc      └──────────────┘
254  
255  @[simp] lemma single_apply {i i' b} : (single i b : Π₀ i, β i) i' = (if h : i = i' then eq.rec_on h b else 0) :=
id                                          └────┘     └┘     └┘   └┘       └┘      └───────┘        
src                                         └────┘       └┘             └┘                └───────┘
typ                                         └────┘     └┘     └┘   └┘       └┘      └───────┘        
doc    └──┘
256  begin
st   └─────
257    dsimp only [single],
id                 └────┘
src    └──────────┘└────┘
typ    └──────────┘└────┘
doc    └──────────┘      
txt    └──────────┘      
par    └──────────┘      
pid         └───┘└┘      
st   ────────────────────┘└─
258    by_cases h : i = i',
id                    └┘
src    └───────┘ └─┘ 
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ────────────────────┘└─
259    { have h1 : i' ∈ finset.singleton i, { simp only [h, finset.mem_singleton] },
id                 └┘  └──────────────┘                  └──────────────────┘
src      └────────┘  └──────────────┘     └─────────┘ └┘└──────────────────┘└┘
typ      └────────┘└┘└──────────────┘    └─────────┘└┘└──────────────────┘└┘
doc      └────────┘   └──────────────┘     └─────────┘ └┘                    └┘
txt      └────────┘                        └─────────┘ └┘                    └┘
par      └────────┘                        └─────────┘ └┘                    └┘
pid      └─────┘└─┘                            └──┘└┘ └┘                    
st   ───┘└───────────────────────────────┘└──┘└──────────────────────────────────┘└┘
260      simp only [mk_apply, dif_pos h, dif_pos h1] },
id                  └──────┘  └─────┘   └─────┘ └┘
src      └─────────┘└──────┘└┘└─────┘ └┘└─────┘  └┘
typ      └─────────┘└──────┘└┘└─────┘└┘└─────┘└┘└┘
doc      └─────────┘        └┘        └┘         └┘
txt      └─────────┘        └┘        └┘         └┘
par      └─────────┘        └┘        └┘         └┘
pid          └──┘└┘        └┘        └┘         
st   ───────────────────────────────────────────────┘└┘
261    { have h1 : i' ∉ finset.singleton i, { simp only [ne.symm h, finset.mem_singleton, not_false_iff] },
id                 └┘   └──────────────┘                └─────┘   └──────────────────┘  └───────────┘
src      └────────┘   └──────────────┘     └─────────┘└─────┘ └┘└──────────────────┘└┘└───────────┘└┘
typ      └────────┘└┘ └──────────────┘    └─────────┘└─────┘└┘└──────────────────┘└┘└───────────┘└┘
doc      └────────┘   └──────────────┘     └─────────┘        └┘                    └┘             └┘
txt      └────────┘                        └─────────┘        └┘                    └┘             └┘
par      └────────┘                        └─────────┘        └┘                    └┘             └┘
pid      └─────┘└─┘                            └──┘└┘        └┘                    └┘             
st   ────────────────────────────────────┘└──┘└─────────────────────────────────────────────────────────┘└┘
262      simp only [mk_apply, dif_neg h, dif_neg h1] }
id                  └──────┘  └─────┘   └─────┘ └┘
src      └─────────┘└──────┘└┘└─────┘ └┘└─────┘  └┘
typ      └─────────┘└──────┘└┘└─────┘└┘└─────┘└┘└┘
doc      └─────────┘        └┘        └┘         └┘
txt      └─────────┘        └┘        └┘         └┘
par      └─────────┘        └┘        └┘         └┘
pid          └──┘└┘        └┘        └┘         
st   ───────────────────────────────────────────────┘└─
263  end
st   ──┘
264  
265  @[simp] lemma single_zero {i} : (single i 0 : Π₀ i, β i) = 0 :=
id                                    └────┘      └┘     
src                                   └────┘       └┘        
typ                                   └────┘      └┘     
doc    └──┘
266  quotient.sound $ λ j, if H : j ∈ finset.singleton i
id   └────────────┘       └┘       └──────────────┘ 
src  └────────────┘        └┘        └──────────────┘
typ  └────────────┘       └┘       └──────────────┘ 
doc                                   └──────────────┘
267  then by dsimp only; rw [dif_pos H]; cases finset.mem_singleton.1 H; refl
id                           └─────┘          └──────────────────┘   
src          └────────┘  └──┘└─────┘   └────┘└──────────────────┘└─┘   └───┘
typ          └────────┘  └──┘└─────┘  └────┘└──────────────────┘└─┘  └───┘
doc          └────────┘  └──┘          └────┘                    └─┘   └───┘
txt          └────────┘  └──┘          └────┘                    └─┘   └───┘
par          └────────┘  └──┘          └────┘                    └─┘   └───┘
pid               └───┘    └┘                                   └─┘       
st          └───────────────┘└───────┘└─────────────────────────────────────┘
268  else dif_neg H
id        └─────┘ 
src       └─────┘
typ       └─────┘ 
269  
270  @[simp] lemma single_eq_same {i b} : (single i b : Π₀ i, β i) i = b :=
id                                         └────┘     └┘       
src                                        └────┘       └┘          
typ                                        └────┘     └┘       
doc    └──┘
271  by simp only [single_apply, dif_pos rfl]
id                 └──────────┘  └─────┘ └─┘
src     └─────────┘└──────────┘└┘└─────┘└─┘└─
typ     └─────────┘└──────────┘└┘└─────┘└─┘└─
doc     └─────────┘            └┘          └─
txt     └─────────┘            └┘          └─
par     └─────────┘            └┘          └─
pid         └──┘└┘            └┘          
st     └──────────────────────────────────────
272  
src  
typ  
doc  
txt  
par  
pid  
st   
273  @[simp] lemma single_eq_of_ne {i i' b} (h : i ≠ i') : (single i b : Π₀ i, β i) i' = 0 :=
id                                                 └┘     └────┘     └┘     └┘ 
src                                                        └────┘       └┘           
typ                                                └┘     └────┘     └┘     └┘ 
doc    └──┘
274  by simp only [single_apply, dif_neg h]
id                 └──────────┘  └─────┘ 
src     └─────────┘└──────────┘└┘└─────┘ └─
typ     └─────────┘└──────────┘└┘└─────┘└─
doc     └─────────┘            └┘        └─
txt     └─────────┘            └┘        └─
par     └─────────┘            └┘        └─
pid         └──┘└┘            └┘        
st     └────────────────────────────────────
275  
src  
typ  
doc  
txt  
par  
pid  
st   
276  def erase (i : ι) (f : Π₀ i, β i) : Π₀ i, β i :=
id                         └┘       └┘   
src                         └┘          └┘  
typ                        └┘       └┘   
277  quotient.lift_on f (λ x, ⟦(⟨λ j, if j = i then 0 else x.1 j, x.2,
id   └──────────────┘                                   
src  └──────────────┘                                           
typ  └──────────────┘                                   
278  λ j, or.cases_on (x.3 j) or.inl $ λ H, or.inr $ by simp only [H, if_t_t]⟩ : pre ι β)⟧) $ λ x y H,
id       └─────────┘      └────┘       └────┘                   └────┘     └─┘           
src       └─────────┘        └────┘        └────┘      └─────────┘ └┘└────┘    └─┘     
typ      └─────────┘      └────┘       └────┘      └─────────┘└┘└────┘    └─┘           
doc                                                     └─────────┘ └┘      
txt                                                     └─────────┘ └┘      
par                                                     └─────────┘ └┘      
pid                                                         └──┘└┘ └┘      
st                                                     └────────────────────┘
279  quotient.sound $ λ j, if h : j = i then by simp only [if_pos h]
id   └────────────┘       └┘                           └────┘ 
src  └────────────┘        └┘                  └─────────┘└────┘ └┘
typ  └────────────┘       └┘                └─────────┘└────┘└┘
doc                                             └─────────┘       └┘
txt                                             └─────────┘       └┘
par                                             └─────────┘       └┘
pid                                                 └──┘└┘       
st                                             └────────────────────┘
280  else by simp only [if_neg h, H j]
id                      └────┘    
src          └─────────┘└────┘ └┘  └─
typ          └─────────┘└────┘└┘└─
doc          └─────────┘       └┘  └─
txt          └─────────┘       └┘  └─
par          └─────────┘       └┘  └─
pid              └──┘└┘       └┘  
st          └──────────────────────────
281  
src  
typ  
doc  
txt  
par  
pid  
st   
282  @[simp] lemma erase_apply {i j : ι} {f : Π₀ i, β i} :
id                                           └┘   
src                                           └┘  
typ                                          └┘   
doc    └──┘
283    (f.erase i) j = if j = i then 0 else f j :=
id      └────┘                        
src      └────┘            
typ     └────┘                        
284  quotient.induction_on f $ λ x, rfl
id   └───────────────────┘        └─┘
src  └───────────────────┘          └─┘
typ  └───────────────────┘        └─┘
285  
286  @[simp] lemma erase_same {i : ι} {f : Π₀ i, β i} : (f.erase i) i = 0 :=
id                                        └┘        └────┘    
src                                        └┘            └────┘      
typ                                       └┘        └────┘    
doc    └──┘
287  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
288  
src  
typ  
doc  
txt  
par  
pid  
st   
289  @[simp] lemma erase_ne {i i' : ι} {f : Π₀ i, β i} (h : i' ≠ i) : (f.erase i) i' = f i' :=
id                                         └┘          └┘       └────┘   └┘   └┘
src                                         └┘                        └────┘       
typ                                        └┘          └┘       └────┘   └┘   └┘
doc    └──┘
290  by simp [h]
id            
src     └────┘ └─
typ     └────┘└─
doc     └────┘ └─
txt     └────┘ └─
par     └────┘ └─
pid          
st     └─────────
291  
src  
typ  
doc  
txt  
par  
pid  
st   
292  end basic
293  
294  section add_monoid
295  
296  variable [Π i, add_monoid (β i)]
id                 └────────┘    
src                 └────────┘
typ                └────────┘    
297  
298  @[simp] lemma single_add {i : ι} {b₁ b₂ : β i} : single i (b₁ + b₂) = single i b₁ + single i b₂ :=
id                                                 └────┘   └┘  └┘   └────┘  └┘  └────┘  └┘
src                                                   └────┘             └────┘       └────┘
typ                                                └────┘   └┘  └┘   └────┘  └┘  └────┘  └┘
doc    └──┘
299  ext $ assume i',
id   └─┘          └┘
src  └─┘
typ  └─┘          └┘
300  begin
st   └─────
301    by_cases h : i = i',
id                    └┘
src    └───────┘ └─┘ 
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ────────────────────┘└─
302    { subst h, simp only [add_apply, single_eq_same] },
id                          └───────┘  └────────────┘
src      └────┘   └─────────┘└───────┘└┘└────────────┘└┘
typ      └────┘  └─────────┘└───────┘└┘└────────────┘└┘
doc      └────┘   └─────────┘         └┘              └┘
txt      └────┘   └─────────┘         └┘              └┘
par      └────┘   └─────────┘         └┘              └┘
pid                  └──┘└┘         └┘              
st   ───┘└─────┘└──────────────────────────────────────┘└┘
303    { simp only [add_apply, single_eq_of_ne h, zero_add] }
id                  └───────┘  └─────────────┘   └──────┘
src      └─────────┘└───────┘└┘└─────────────┘ └┘└──────┘└┘
typ      └─────────┘└───────┘└┘└─────────────┘└┘└──────┘└┘
doc      └─────────┘         └┘                └┘        └┘
txt      └─────────┘         └┘                └┘        └┘
par      └─────────┘         └┘                └┘        └┘
pid          └──┘└┘         └┘                └┘        
st   ──────────────────────────────────────────────────────┘└─
304  end
st   ──┘
305  
306  lemma single_add_erase {i : ι} {f : Π₀ i, β i} : single i (f i) + f.erase i = f :=
id                                      └┘       └────┘       └────┘   
src                                      └┘          └────┘           └────┘   
typ                                     └┘       └────┘       └────┘   
307  ext $ λ i',
id   └─┘     └┘
src  └─┘
typ  └─┘     └┘
308  if h : i = i' then by subst h; simp only [add_apply, single_apply, erase_apply, dif_pos rfl, if_pos, add_zero]
id   └┘       └┘                            └───────┘  └──────────┘  └─────────┘  └─────┘ └─┘  └────┘  └──────┘
src  └┘                   └────┘   └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘└─┘└┘└────┘└┘└──────┘└┘
typ  └┘       └┘         └────┘  └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘└─┘└┘└────┘└┘└──────┘└┘
doc                        └────┘   └─────────┘         └┘            └┘           └┘          └┘      └┘        └┘
txt                        └────┘   └─────────┘         └┘            └┘           └┘          └┘      └┘        └┘
par                        └────┘   └─────────┘         └┘            └┘           └┘          └┘      └┘        └┘
pid                                    └──┘└┘         └┘            └┘           └┘          └┘      └┘        
st                        └────────────────────────────────────────────────────────────────────────────────────────┘
309  else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (ne.symm h), zero_add]
id                      └───────┘  └──────────┘  └─────────┘  └─────┘   └────┘  └─────┘    └──────┘
src          └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘ └┘└────┘ └─────┘ └─┘└──────┘└─
typ          └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘└┘└────┘ └─────┘└─┘└──────┘└─
doc          └─────────┘         └┘            └┘           └┘        └┘               └─┘        └─
txt          └─────────┘         └┘            └┘           └┘        └┘               └─┘        └─
par          └─────────┘         └┘            └┘           └┘        └┘               └─┘        └─
pid              └──┘└┘         └┘            └┘           └┘        └┘               └─┘        
st          └──────────────────────────────────────────────────────────────────────────────────────────
310  
src  
typ  
doc  
txt  
par  
pid  
st   
311  lemma erase_add_single {i : ι} {f : Π₀ i, β i} : f.erase i + single i (f i) = f :=
id                                      └┘       └────┘   └────┘       
src                                      └┘           └────┘    └────┘         
typ                                     └┘       └────┘   └────┘       
312  ext $ λ i',
id   └─┘     └┘
src  └─┘
typ  └─┘     └┘
313  if h : i = i' then by subst h; simp only [add_apply, single_apply, erase_apply, dif_pos rfl, if_pos, zero_add]
id   └┘       └┘                            └───────┘  └──────────┘  └─────────┘  └─────┘ └─┘  └────┘  └──────┘
src  └┘                   └────┘   └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘└─┘└┘└────┘└┘└──────┘└┘
typ  └┘       └┘         └────┘  └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘└─┘└┘└────┘└┘└──────┘└┘
doc                        └────┘   └─────────┘         └┘            └┘           └┘          └┘      └┘        └┘
txt                        └────┘   └─────────┘         └┘            └┘           └┘          └┘      └┘        └┘
par                        └────┘   └─────────┘         └┘            └┘           └┘          └┘      └┘        └┘
pid                                    └──┘└┘         └┘            └┘           └┘          └┘      └┘        
st                        └────────────────────────────────────────────────────────────────────────────────────────┘
314  else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (ne.symm h), add_zero]
id                      └───────┘  └──────────┘  └─────────┘  └─────┘   └────┘  └─────┘    └──────┘
src          └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘ └┘└────┘ └─────┘ └─┘└──────┘└─
typ          └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘└┘└────┘ └─────┘└─┘└──────┘└─
doc          └─────────┘         └┘            └┘           └┘        └┘               └─┘        └─
txt          └─────────┘         └┘            └┘           └┘        └┘               └─┘        └─
par          └─────────┘         └┘            └┘           └┘        └┘               └─┘        └─
pid              └──┘└┘         └┘            └┘           └┘        └┘               └─┘        
st          └──────────────────────────────────────────────────────────────────────────────────────────
315  
src  
typ  
doc  
txt  
par  
pid  
st   
316  protected theorem induction {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i)
id                                     └┘                  └┘   
src                                    └┘                     └┘  
typ                                    └┘                  └┘   
317    (h0 : p 0) (ha : ∀i b (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)) :
id                             └┘                         └────┘    
src                               └┘                                  └────┘     
typ                            └┘                         └────┘    
318    p f :=
id      
typ     
319  begin
st   └─────
320    refine quotient.induction_on f (λ x, _),
id            └───────────────────┘ 
src    └─────┘└───────────────────┘   └────┘
typ    └─────┘└───────────────────┘  └────┘
doc    └─────┘                        └────┘
txt    └─────┘                        └────┘
par    └─────┘                        └────┘
pid                                  └────┘
st   ────────────────────────────────────────┘└─
321    cases x with f s H, revert f H,
id           
src    └────┘ └─────────┘  └────────┘
typ    └────┘└─────────┘  └────────┘
doc    └────┘ └─────────┘  └────────┘
txt    └────┘ └─────────┘  └────────┘
par    └────┘ └─────────┘  └────────┘
pid          └─────────┘        └──┘
st   ───────────────────┘└──────────┘└─
322    apply multiset.induction_on s,
id           └───────────────────┘ 
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ──────────────────────────────┘└─
323    { intros f H, convert h0, ext i, exact (H i).resolve_left id },
id                           └┘                                └┘
src      └────────┘  └──────┘    └───┘  └────┘   └─────────────┘└┘
typ      └────────┘  └──────┘└┘  └───┘  └────┘ └─────────────┘└┘
doc      └────────┘  └──────┘    └───┘  └────┘   └─────────────┘  
txt      └────────┘  └──────┘    └───┘  └────┘   └─────────────┘  
par      └────────┘  └──────┘    └───┘  └────┘   └─────────────┘  
pid            └──┘                └┘          └─────────────┘  
st   ───┘└────────┘└──────────┘└─────┘└────────────────────────────┘└┘
324    intros i s ih f H,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid          └─────────┘
st   ──────────────────┘└─
325    by_cases H1 : i ∈ s,
id                     
src    └───────┘  └─┘ 
typ    └───────┘  └─┘
doc    └───────┘  └─┘  
txt    └───────┘  └─┘  
par    └───────┘  └─┘  
pid              └─┘  
st   ────────────────────┘└─
326    { have H2 : ∀ j, j ∈ s ∨ f j = 0,
id                                
src      └────────┘ └┘       └┘
typ      └────────┘ └┘     └┘
doc      └────────┘ └┘        └┘
txt      └────────┘ └┘        └┘
par      └────────┘ └┘        └┘
pid      └─────┘└─┘ └┘        
st   ───┘└────────────────────────────┘└─
327      { intro j, cases H j with H2 H2,
id                         
src        └─────┘  └────┘  └─────────┘
typ        └─────┘  └────┘└─────────┘
doc        └─────┘  └────┘  └─────────┘
txt        └─────┘  └────┘  └─────────┘
par        └─────┘  └────┘  └─────────┘
pid             └┘         └─────────┘
st   ─────┘└─────┘└────────────────────┘└─
328        { cases multiset.mem_cons.1 H2 with H3 H3,
id                 └───────────────┘   └┘
src          └────┘└───────────────┘└─┘  └─────────┘
typ          └────┘└───────────────┘└─┘└┘└─────────┘
doc          └────┘                 └─┘  └─────────┘
txt          └────┘                 └─┘  └─────────┘
par          └────┘                 └─┘  └─────────┘
pid                                └─┘  └─────────┘
st   ───────┘└─────────────────────────────────────┘└─
329          { left, rw H3, exact H1 },
id                      └┘        └┘
src            └──┘  └─┘    └────┘  
typ            └──┘  └─┘└┘  └────┘└┘
doc            └──┘  └─┘    └────┘  
txt            └──┘  └─┘    └────┘  
par            └──┘  └─┘    └────┘  
pid                               
st   ─────────┘└──┘└─────┘└─────────┘└┘
330          { left, exact H3 } },
id                         └┘
src            └──┘  └────┘  
typ            └──┘  └────┘└┘
doc            └──┘  └────┘  
txt            └──┘  └────┘  
par            └──┘  └────┘  
pid                         
st   ─────────────┘└─────────┘└──┘
331        right, exact H2 },
id                      └┘
src        └───┘  └────┘  
typ        └───┘  └────┘└┘
doc        └───┘  └────┘  
txt        └───┘  └────┘  
par        └───┘  └────┘  
pid                      
st   ──────────┘└─────────┘└┘
332      have H3 : (⟦{to_fun := f, pre_support := i :: s, zero := H}⟧ : Π₀ i, β i)
id                                                └┘                └┘   
src      └────────┘  └────────┘ └───────────────┘ └┘ └────────┘ └─┘└┘└┘  └─
typ      └────────┘  └────────┘ └───────────────┘└┘ └────────┘└─┘└┘└┘ └─
doc      └────────┘   └────────┘ └───────────────┘ └┘ └────────┘  └─┘  └┘   └─
txt      └────────┘   └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └─
par      └────────┘   └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └─
pid      └─────┘└─┘   └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └─
st   ──────────────────────────────────────────────────────────────────────────────
333        = ⟦{to_fun := f, pre_support := s, zero := H2}⟧,
id                                                  └┘
src  ─────┘   └────────┘ └───────────────┘ └────────┘  
typ  ─────┘   └────────┘└───────────────┘└────────┘└┘
doc  ─────┘   └────────┘ └───────────────┘ └────────┘  
txt  ─────┘   └────────┘ └───────────────┘ └────────┘  
par  ─────┘   └────────┘ └───────────────┘ └────────┘  
pid  ─────┘   └────────┘ └───────────────┘ └────────┘  
st   ────────────────────────────────────────────────────┘└─
334      { exact quotient.sound (λ i, rfl) },
id               └────────────┘       └─┘
src        └────┘└────────────┘  └──┘└─┘└┘
typ        └────┘└────────────┘  └──┘└─┘└┘
doc        └────┘                └──┘   └┘
txt        └────┘                └──┘   └┘
par        └────┘                └──┘   └┘
pid                             └──┘   
st   ─────┘└──────────────────────────────┘└┘
335      rw H3, apply ih },
id          └┘
src      └─┘    └────┘  
typ      └─┘└┘  └────┘  
doc      └─┘    └────┘  
txt      └─┘    └────┘  
par      └─┘    └────┘  
pid                   
st   ────────┘└─────────┘└┘
336    have H2 : p (erase i ⟦{to_fun := f, pre_support := i :: s, zero := H}⟧),
id                 └───┘                                              
src    └────────┘  └───┘   └────────┘ └───────────────┘    └────────┘  
typ    └────────┘ └───┘   └────────┘└───────────────┘  └────────┘ 
doc    └────────┘          └────────┘ └───────────────┘    └────────┘  
txt    └────────┘          └────────┘ └───────────────┘    └────────┘  
par    └────────┘          └────────┘ └───────────────┘    └────────┘  
pid    └─────┘└─┘          └────────┘ └───────────────┘    └────────┘  
st   ────────────────────────────────────────────────────────────────────────┘└─
337    { dsimp only [erase, quotient.lift_on_beta],
id                   └───┘  └───────────────────┘
src      └──────────┘└───┘└┘└───────────────────┘
typ      └──────────┘└───┘└┘└───────────────────┘
doc      └──────────┘     └┘                     
txt      └──────────┘     └┘                     
par      └──────────┘     └┘                     
pid           └───┘└┘     └┘                     
st   ───┘└───────────────────────────────────────┘└─
338      have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0,
id                             └─┘           
src      └────────┘ └┘     └─┘    └──┘   └┘ └┘
typ      └────────┘ └┘    └─┘   └──┘  └┘ └┘
doc      └────────┘ └┘            └──┘   └┘ └┘
txt      └────────┘ └┘            └──┘   └┘ └┘
par      └────────┘ └┘            └──┘   └┘ └┘
pid      └─────┘└─┘ └┘            └──┘   └┘ 
st   ─────────────────────────────────────────────────┘└─
339      { intro j, cases H j with H2 H2,
id                         
src        └─────┘  └────┘  └─────────┘
typ        └─────┘  └────┘└─────────┘
doc        └─────┘  └────┘  └─────────┘
txt        └─────┘  └────┘  └─────────┘
par        └─────┘  └────┘  └─────────┘
pid             └┘         └─────────┘
st   ─────┘└─────┘└────────────────────┘└─
340        { cases multiset.mem_cons.1 H2 with H3 H3,
id                 └───────────────┘   └┘
src          └────┘└───────────────┘└─┘  └─────────┘
typ          └────┘└───────────────┘└─┘└┘└─────────┘
doc          └────┘                 └─┘  └─────────┘
txt          └────┘                 └─┘  └─────────┘
par          └────┘                 └─┘  └─────────┘
pid                                └─┘  └─────────┘
st   ───────┘└─────────────────────────────────────┘└─
341          { right, exact if_pos H3 },
id                          └────┘ └┘
src            └───┘  └────┘└────┘  
typ            └───┘  └────┘└────┘└┘
doc            └───┘  └────┘        
txt            └───┘  └────┘        
par            └───┘  └────┘        
pid                                
st   ─────────┘└───┘└────────────────┘└┘
342          { left, exact H3 } },
id                         └┘
src            └──┘  └────┘  
typ            └──┘  └────┘└┘
doc            └──┘  └────┘  
txt            └──┘  └────┘  
par            └──┘  └────┘  
pid                         
st   ─────────────┘└─────────┘└──┘
343        right, split_ifs; [refl, exact H2] },
id                                       └┘
src        └───┘  └───────┘  └──┘  └────┘
typ        └───┘  └───────┘  └──┘  └────┘└┘
doc        └───┘  └───────┘   └──┘  └────┘
txt        └───┘  └───────┘   └──┘  └────┘
par        └───┘  └───────┘   └──┘  └────┘
pid                                      
st   ──────────┘└───────────────────────────┘└─┘
344      have H3 : (⟦{to_fun := λ (j : ι), ite (j = i) 0 (f j), pre_support := i :: s, zero := _}⟧ : Π₀ i, β i)
id                                                                                                   └┘   
src      └────────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘    └──────────┘ └─┘└┘└┘  └─
typ      └────────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘    └──────────┘ └─┘└┘└┘ └─
doc      └────────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘    └──────────┘ └─┘  └┘   └─
txt      └────────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘    └──────────┘ └─┘  └┘   └─
par      └────────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘    └──────────┘ └─┘  └┘   └─
pid      └─────┘└─┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘    └──────────┘ └─┘  └┘   └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────
345        = ⟦{to_fun := λ (j : ι), ite (j = i) 0 (f j), pre_support := s, zero := H2}⟧ :=
id                                 └─┘                                         └┘
src  ─────┘   └────────┘ └────┘ └─┘└─┘    └──┘   └────────────────┘ └────────┘   └───
typ  ─────┘   └────────┘ └────┘└─┘└─┘   └──┘  └────────────────┘└────────┘└┘ └───
doc  ─────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘ └────────┘   └───
txt  ─────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘ └────────┘   └───
par  ─────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘ └────────┘   └───
pid  ─────┘   └────────┘ └────┘ └─┘       └──┘   └────────────────┘ └────────┘   └───
st   ──────────────────────────────────────────────────────────────────────────────────────
346        quotient.sound (λ i, rfl),
id         └────────────┘       └─┘
src  ─────┘└────────────┘  └──┘└─┘
typ  ─────┘└────────────┘  └──┘└─┘
doc  ─────┘                └──┘   
txt  ─────┘                └──┘   
par  ─────┘                └──┘   
pid  ─────┘                └──┘   
st   ──────────────────────────────┘└─
347      rw H3, apply ih },
id          └┘
src      └─┘    └────┘  
typ      └─┘└┘  └────┘  
doc      └─┘    └────┘  
txt      └─┘    └────┘  
par      └─┘    └────┘  
pid                   
st   ────────┘└─────────┘└┘
348    have H3 : single i _ + _ = (⟦{to_fun := f, pre_support := i :: s, zero := H}⟧ : Π₀ i, β i) := single_add_erase,
id               └────┘                                                           └┘          └──────────────┘
src    └────────┘└────┘ └─┘└─┘    └────────┘ └───────────────┘    └────────┘  └─┘└┘└┘  └───┘└──────────────┘
typ    └────────┘└────┘ └─┘└─┘    └────────┘└───────────────┘  └────────┘ └─┘└┘└┘ └───┘└──────────────┘
doc    └────────┘       └─┘ └─┘    └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └───┘
txt    └────────┘       └─┘ └─┘    └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └───┘
par    └────────┘       └─┘ └─┘    └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └───┘
pid    └─────┘└─┘       └─┘ └─┘    └────────┘ └───────────────┘    └────────┘  └─┘  └┘   └──┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
349    rw ← H3,
id          └┘
src    └───┘
typ    └───┘└┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ────────┘└─
350    change p (single i (f i) + _),
id              └────┘     
src    └─────┘  └────┘    └┘ └─┘
typ    └─────┘ └────┘  └┘ └─┘
doc    └─────┘            └┘ └─┘
txt    └─────┘            └┘ └─┘
par    └─────┘            └┘ └─┘
pid                      └┘ └─┘
st   ──────────────────────────────┘└─
351    cases classical.em (f i = 0) with h h,
id           └──────────┘   
src    └────┘└──────────┘    └──────────┘
typ    └────┘└──────────┘  └──────────┘
doc    └────┘                └──────────┘
txt    └────┘                └──────────┘
par    └────┘                └──────────┘
pid                         └─┘└───────┘
st   ──────────────────────────────────────┘└─
352    { rw [h, single_zero, zero_add], exact H2 },
id             └─────────┘  └──────┘         └┘
src      └──┘ └┘└─────────┘└┘└──────┘  └────┘  
typ      └──┘└┘└─────────┘└┘└──────┘  └────┘└┘
doc      └──┘ └┘           └┘          └────┘  
txt      └──┘ └┘           └┘          └────┘  
par      └──┘ └┘           └┘          └────┘  
pid        └┘ └┘           └┘                 
st   ───┘└───┘└───────────┘└────────┘└─────────┘└┘
353    refine ha _ _ _ _ h H2,
id            └┘          └┘
src    └─────┘  └───────┘ 
typ    └─────┘└┘└───────┘└┘
doc    └─────┘  └───────┘ 
txt    └─────┘  └───────┘ 
par    └─────┘  └───────┘ 
pid            └───────┘ 
st   ───────────────────────┘└─
354    rw erase_same
id        └────────┘
src    └─┘└────────┘
typ    └─┘└────────┘
doc    └─┘          
txt    └─┘          
par    └─┘          
pid                
st   ───────────────┘
355  end
st   └─┘
356  
357  lemma induction₂ {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i)
id                          └┘                  └┘   
src                         └┘                     └┘  
typ                         └┘                  └┘   
358    (h0 : p 0) (ha : ∀i b (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)) :
id                             └┘                           └────┘  
src                               └┘                                     └────┘
typ                            └┘                           └────┘  
359    p f :=
id      
typ     
360  dfinsupp.induction f h0 $ λ i b f h1 h2 h3,
id   └────────────────┘  └┘        └┘ └┘ └┘
src  └────────────────┘
typ  └────────────────┘  └┘        └┘ └┘ └┘
361  have h4 : f + single i b = single i b + f,
id               └────┘    └────┘    
src               └────┘      └────┘     
typ              └────┘    └────┘    
362  { ext j, by_cases H : i = j,
id                           
src    └───┘  └───────┘ └─┘ 
typ    └───┘  └───────┘ └─┘
doc    └───┘  └───────┘ └─┘  
txt    └───┘  └───────┘ └─┘  
par    └───┘  └───────┘ └─┘  
pid       └┘           └─┘  
st   └─────┘└──────────────────┘└─
363    { subst H, simp [h1] },
id                     └┘
src      └────┘   └────┘  └┘
typ      └────┘  └────┘└┘└┘
doc      └────┘   └────┘  └┘
txt      └────┘   └────┘  └┘
par      └────┘   └────┘  └┘
pid                    
st   ───┘└─────┘└──────────┘└┘
364    { simp [H] } },
id             
src      └────┘ └┘
typ      └────┘└┘
doc      └────┘ └┘
txt      └────┘ └┘
par      └────┘ └┘
pid           
st   ────────────┘└──┘
365  eq.rec_on h4 $ ha i b f h1 h2 h3
id   └───────┘ └┘   └┘    └┘ └┘ └┘
src  └───────┘
typ  └───────┘ └┘   └┘    └┘ └┘ └┘
366  
367  end add_monoid
368  
369  @[simp] lemma mk_add [Π i, add_monoid (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i.1} :
id                             └────────┘           └────┘                   └─┘     
src                             └────────┘             └────┘                      └─┘        
typ                            └────────┘           └────┘                   └─┘     
doc    └──┘                                            └────┘
370    mk s (x + y) = mk s x + mk s y :=
id     └┘        └┘    └┘  
src    └┘           └┘      └┘
typ    └┘        └┘    └┘  
371  ext $ λ i, by simp only [add_apply, mk_apply]; split_ifs; [refl, rw zero_add]
id   └─┘                     └───────┘  └──────┘                       └──────┘
src  └─┘           └─────────┘└───────┘└┘└──────┘  └───────┘  └──┘  └─┘└──────┘
typ  └─┘          └─────────┘└───────┘└┘└──────┘  └───────┘  └──┘  └─┘└──────┘
doc                └─────────┘         └┘          └───────┘   └──┘  └─┘
txt                └─────────┘         └┘          └───────┘   └──┘  └─┘
par                └─────────┘         └┘          └───────┘   └──┘  └─┘
pid                    └──┘└┘         └┘                              
st                └─────────────────────────────────────────────────────┘└──────┘
372  
373  @[simp] lemma mk_zero [Π i, has_zero (β i)] {s : finset ι} :
id                              └──────┘           └────┘ 
src                              └──────┘             └────┘
typ                             └──────┘           └────┘ 
doc    └──┘                                           └────┘
374    mk s (0 : Π i : (↑s : set ι), β i.1) = 0 :=
id     └┘                └─┘        
src    └┘                   └─┘           
typ    └┘                └─┘        
375  ext $ λ i, by simp only [mk_apply]; split_ifs; refl
id   └─┘                     └──────┘
src  └─┘           └─────────┘└──────┘  └───────┘  └────
typ  └─┘          └─────────┘└──────┘  └───────┘  └────
doc                └─────────┘          └───────┘  └────
txt                └─────────┘          └───────┘  └────
par                └─────────┘          └───────┘  └────
pid                    └──┘└┘                         
st                └──────────────────────────────────────
376  
src  
typ  
doc  
txt  
par  
pid  
st   
377  @[simp] lemma mk_neg [Π i, add_group (β i)] {s : finset ι} {x : Π i : (↑s : set ι), β i.1} :
id                             └───────┘           └────┘                 └─┘     
src                             └───────┘             └────┘                    └─┘        
typ                            └───────┘           └────┘                 └─┘     
doc    └──┘                                           └────┘
378    mk s (-x) = -mk s x :=
id     └┘      └┘  
src    └┘        └┘
typ    └┘      └┘  
379  ext $ λ i, by simp only [neg_apply, mk_apply]; split_ifs; [refl, rw neg_zero]
id   └─┘                     └───────┘  └──────┘                       └──────┘
src  └─┘           └─────────┘└───────┘└┘└──────┘  └───────┘  └──┘  └─┘└──────┘
typ  └─┘          └─────────┘└───────┘└┘└──────┘  └───────┘  └──┘  └─┘└──────┘
doc                └─────────┘         └┘          └───────┘   └──┘  └─┘
txt                └─────────┘         └┘          └───────┘   └──┘  └─┘
par                └─────────┘         └┘          └───────┘   └──┘  └─┘
pid                    └──┘└┘         └┘                              
st                └─────────────────────────────────────────────────────┘└──────┘
380  
381  @[simp] lemma mk_sub [Π i, add_group (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i.1} :
id                             └───────┘           └────┘                   └─┘     
src                             └───────┘             └────┘                      └─┘        
typ                            └───────┘           └────┘                   └─┘     
doc    └──┘                                           └────┘
382    mk s (x - y) = mk s x - mk s y :=
id     └┘        └┘    └┘  
src    └┘           └┘      └┘
typ    └┘        └┘    └┘  
383  ext $ λ i, by simp only [sub_apply, mk_apply]; split_ifs; [refl, rw sub_zero]
id   └─┘                     └───────┘  └──────┘                       └──────┘
src  └─┘           └─────────┘└───────┘└┘└──────┘  └───────┘  └──┘  └─┘└──────┘
typ  └─┘          └─────────┘└───────┘└┘└──────┘  └───────┘  └──┘  └─┘└──────┘
doc                └─────────┘         └┘          └───────┘   └──┘  └─┘
txt                └─────────┘         └┘          └───────┘   └──┘  └─┘
par                └─────────┘         └┘          └───────┘   └──┘  └─┘
pid                    └──┘└┘         └┘                              
st                └─────────────────────────────────────────────────────┘└──────┘
384  
385  instance [Π i, add_group (β i)] {s : finset ι} : is_add_group_hom (@mk ι β _ _ s) :=
id                 └───────┘           └────┘     └──────────────┘   └┘       
src                 └───────┘             └────┘      └──────────────┘   └┘
typ                └───────┘           └────┘     └──────────────┘   └┘       
doc                                       └────┘      └──────────────┘
386  { map_add := λ _ _, mk_add }
id                     └────┘
src                      └────┘
typ                    └────┘
387  
388  section
389  local attribute [instance] to_module
id                              └───────┘
src                             └───────┘
typ                             └───────┘
390  variables (γ : Type w) [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
id                           └──┘         └────────────┘            └────┘      
src                          └──┘          └────────────┘              └────┘
typ                          └──┘         └────────────┘            └────┘      
doc                                                                    └────┘
391  include γ
392  @[simp] lemma mk_smul {s : finset ι} {c : γ} (x : Π i : (↑s : set ι), β i.1) :
id                              └────┘                        └─┘     
src                             └────┘                            └─┘        
typ                             └────┘                        └─┘     
doc    └──┘                     └────┘
393    mk s (c • x) = c • mk s x :=
id     └┘          └┘  
src    └┘              └┘
typ    └┘          └┘  
394  ext $ λ i, by simp only [smul_apply, mk_apply]; split_ifs; [refl, rw smul_zero]
id   └─┘                     └────────┘  └──────┘                       └───────┘
src  └─┘           └─────────┘└────────┘└┘└──────┘  └───────┘  └──┘  └─┘└───────┘
typ  └─┘          └─────────┘└────────┘└┘└──────┘  └───────┘  └──┘  └─┘└───────┘
doc                └─────────┘          └┘          └───────┘   └──┘  └─┘
txt                └─────────┘          └┘          └───────┘   └──┘  └─┘
par                └─────────┘          └┘          └───────┘   └──┘  └─┘
pid                    └──┘└┘          └┘                              
st                └──────────────────────────────────────────────────────┘└───────┘
395  
396  @[simp] lemma single_smul {i : ι} {c : γ} {x : β i} :
id                                                 
typ                                                
doc    └──┘
397    single i (c • x) = c • single i x :=
id     └────┘          └────┘  
src    └────┘              └────┘
typ    └────┘          └────┘  
398  ext $ λ i, by simp only [smul_apply, single_apply]; split_ifs; [cases h, rw smul_zero]; refl
id   └─┘                     └────────┘  └──────────┘                         └───────┘
src  └─┘           └─────────┘└────────┘└┘└──────────┘  └───────┘  └────┘   └─┘└───────┘   └────
typ  └─┘          └─────────┘└────────┘└┘└──────────┘  └───────┘  └────┘  └─┘└───────┘   └────
doc                └─────────┘          └┘              └───────┘   └────┘   └─┘            └────
txt                └─────────┘          └┘              └───────┘   └────┘   └─┘            └────
par                └─────────┘          └┘              └───────┘   └────┘   └─┘            └────
pid                    └──┘└┘          └┘                                                    
st                └─────────────────────────────────────────────────────────────┘└───────┘└───────
399  
src  
typ  
doc  
txt  
par  
pid  
st   
400  variable β
401  def lmk (s : finset ι) : (Π i : (↑s : set ι), β i.1) →ₗ[γ] Π₀ i, β i :=
id                └────┘               └─┘        └─┘ └┘   
src               └────┘                  └─┘           └─┘  └┘  
typ               └────┘               └─┘        └─┘ └┘   
doc               └────┘
402  ⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul γ x]⟩
id    └┘        └────┘              └─────┘  
src   └┘           └────┘            └──┘└─────┘  
typ   └┘        └────┘          └──┘└─────┘
doc                                  └──┘         
txt                                  └──┘         
par                                  └──┘         
pid                                    └┘         
st                                  └──────────────┘
403  
404  def lsingle (i) : β i →ₗ[γ] Π₀ i, β i :=
id                       └─┘ └┘   
src                        └─┘  └┘  
typ                      └─┘ └┘   
405  ⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩
id    └────┘        └────────┘       └─────────┘
src   └────┘           └────────┘         └─────────┘
typ   └────┘        └────────┘       └─────────┘
406  variable {β}
407  
408  @[simp] lemma lmk_apply {s : finset ι} {x} : lmk β γ s x = mk s x := rfl
id                                └────┘         └─┘      └┘      └─┘
src                               └────┘          └─┘          └┘        └─┘
typ                               └────┘         └─┘      └┘      └─┘
doc    └──┘                       └────┘
409  
410  @[simp] lemma lsingle_apply {i : ι} {x : β i} : lsingle β γ i x = single i x := rfl
id                                                └─────┘      └────┘      └─┘
src                                                  └─────┘          └────┘        └─┘
typ                                               └─────┘      └────┘      └─┘
doc    └──┘
411  end
412  
413  section support_basic
414  
415  variables [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                  └──────┘            └────────────┘  └┘        
src                  └──────┘              └────────────┘  └┘
typ                 └──────┘            └────────────┘  └┘        
416  
417  def support (f : Π₀ i, β i) : finset ι :=
id                    └┘       └────┘ 
src                   └┘          └────┘
typ                   └┘       └────┘ 
doc                                └────┘
418  quotient.lift_on f (λ x, x.2.to_finset.filter $ λ i, x.1 i ≠ 0) $
id   └──────────────┘        └───────┘ └────┘           
src  └──────────────┘           └───────┘ └────┘              
typ  └──────────────┘        └───────┘ └────┘           
doc                              └───────┘ └────┘
419  begin
st   └─────
420    intros x y Hxy,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
421    ext i, split,
src    └───┘  └───┘
typ    └───┘  └───┘
doc    └───┘  └───┘
txt    └───┘  └───┘
par    └───┘  └───┘
pid       └┘
st   ──────┘└─────┘└─
422    { intro H,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
423      rcases finset.mem_filter.1 H with ⟨h1, h2⟩,
id              └───────────────┘   
src      └─────┘└───────────────┘└─┘ └────────────┘
typ      └─────┘└───────────────┘└─┘└────────────┘
doc      └─────┘                 └─┘ └────────────┘
txt      └─────┘                 └─┘ └────────────┘
par      └─────┘                 └─┘ └────────────┘
pid                             └─┘ └────────────┘
st   ─────────────────────────────────────────────┘└─
424      rw Hxy i at h2,
id          └─┘ 
src      └─┘    └────┘
typ      └─┘└─┘└────┘
doc      └─┘    └────┘
txt      └─┘    └────┘
par      └─┘    └────┘
pid            └────┘
st   ─────────────────┘└─
425      exact finset.mem_filter.2 ⟨multiset.mem_to_finset.2 $ (y.3 i).resolve_right h2, h2⟩ },
id             └───────────────┘    └────────────────────┘                             └┘
src      └────┘└───────────────┘└─┘ └────────────────────┘└─┘   └─┘ └──────────────┘  └┘  └┘
typ      └────┘└───────────────┘└─┘ └────────────────────┘└─┘  └─┘└──────────────┘  └┘└┘└┘
doc      └────┘                 └─┘                       └─┘   └─┘ └──────────────┘  └┘  └┘
txt      └────┘                 └─┘                       └─┘   └─┘ └──────────────┘  └┘  └┘
par      └────┘                 └─┘                       └─┘   └─┘ └──────────────┘  └┘  └┘
pid                            └─┘                       └─┘   └─┘ └──────────────┘  └┘  
st   ───────────────────────────────────────────────────────────────────────────────────────┘└┘
426    { intro H,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
427      rcases finset.mem_filter.1 H with ⟨h1, h2⟩,
id              └───────────────┘   
src      └─────┘└───────────────┘└─┘ └────────────┘
typ      └─────┘└───────────────┘└─┘└────────────┘
doc      └─────┘                 └─┘ └────────────┘
txt      └─────┘                 └─┘ └────────────┘
par      └─────┘                 └─┘ └────────────┘
pid                             └─┘ └────────────┘
st   ─────────────────────────────────────────────┘└─
428      rw ← Hxy i at h2,
id            └─┘ 
src      └───┘    └────┘
typ      └───┘└─┘└────┘
doc      └───┘    └────┘
txt      └───┘    └────┘
par      └───┘    └────┘
pid        └─┘    └────┘
st   ───────────────────┘└─
429      exact finset.mem_filter.2 ⟨multiset.mem_to_finset.2 $ (x.3 i).resolve_right h2, h2⟩ },
id             └───────────────┘    └────────────────────┘                             └┘
src      └────┘└───────────────┘└─┘ └────────────────────┘└─┘   └─┘ └──────────────┘  └┘  └┘
typ      └────┘└───────────────┘└─┘ └────────────────────┘└─┘  └─┘└──────────────┘  └┘└┘└┘
doc      └────┘                 └─┘                       └─┘   └─┘ └──────────────┘  └┘  └┘
txt      └────┘                 └─┘                       └─┘   └─┘ └──────────────┘  └┘  └┘
par      └────┘                 └─┘                       └─┘   └─┘ └──────────────┘  └┘  └┘
pid                            └─┘                       └─┘   └─┘ └──────────────┘  └┘  
st   ───────────────────────────────────────────────────────────────────────────────────────┘└──
430  end
st   ──┘
431  
432  @[simp] theorem support_mk_subset {s : finset ι} {x : Π i : (↑s : set ι), β i.1} : (mk s x).support ⊆ s :=
id                                          └────┘                 └─┘           └┘   └─────┘   
src                                         └────┘                    └─┘              └┘     └─────┘  
typ                                         └────┘                 └─┘           └┘   └─────┘   
doc    └──┘                                 └────┘
433  λ i H, multiset.mem_to_finset.1 (finset.mem_filter.1 H).1
id        └────────────────────┘   └───────────────┘   
src         └────────────────────┘   └───────────────┘    
typ       └────────────────────┘   └───────────────┘   
434  
435  @[simp] theorem mem_support_to_fun (f : Π₀ i, β i) (i) : i ∈ f.support ↔ f i ≠ 0 :=
id                                           └┘             └──────┘    
src                                          └┘                  └──────┘      
typ                                          └┘             └──────┘    
doc    └──┘
436  begin
st   └─────
437    refine quotient.induction_on f (λ x, _),
id            └───────────────────┘ 
src    └─────┘└───────────────────┘   └────┘
typ    └─────┘└───────────────────┘  └────┘
doc    └─────┘                        └────┘
txt    └─────┘                        └────┘
par    └─────┘                        └────┘
pid                                  └────┘
st   ────────────────────────────────────────┘└─
438    dsimp only [support, quotient.lift_on_beta],
id                 └─────┘  └───────────────────┘
src    └──────────┘└─────┘└┘└───────────────────┘
typ    └──────────┘└─────┘└┘└───────────────────┘
doc    └──────────┘       └┘                     
txt    └──────────┘       └┘                     
par    └──────────┘       └┘                     
pid         └───┘└┘       └┘                     
st   ────────────────────────────────────────────┘└─
439    rw [finset.mem_filter, multiset.mem_to_finset],
id         └───────────────┘  └────────────────────┘
src    └──┘└───────────────┘└┘└────────────────────┘
typ    └──┘└───────────────┘└┘└────────────────────┘
doc    └──┘                 └┘                      
txt    └──┘                 └┘                      
par    └──┘                 └┘                      
pid      └┘                 └┘                      
st   ──────────────────────┘└──────────────────────┘└──
440    exact and_iff_right_of_imp (x.3 i).resolve_right
id           └──────────────────┘     
src    └────┘└──────────────────┘  └─┘ └──────────────┘
typ    └────┘└──────────────────┘ └─┘└──────────────┘
doc    └────┘                      └─┘ └──────────────┘
txt    └────┘                      └─┘ └──────────────┘
par    └────┘                      └─┘ └──────────────┘
pid                               └─┘ └────────────┘└┘
st   ──────────────────────────────────────────────────┘
441  end
st   └─┘
442  
443  theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support (λ i, f i.1) :=
id                              └┘         └┘ └──────┘       
src                             └┘             └┘  └──────┘          
typ                             └┘         └┘ └──────┘       
444  by ext i; by_cases h : f i = 0; try {simp at h}; simp [h]
id                                                       
src     └───┘  └───────┘ └─┘  └┘  └───┘└───────┘  └────┘ └─
typ     └───┘  └───────┘ └─┘└┘  └───┘└───────┘  └────┘└─
doc     └───┘  └───────┘ └─┘   └┘  └───┘└───────┘  └────┘ └─
txt     └───┘  └───────┘ └─┘   └┘  └───┘└───────┘  └────┘ └─
par     └───┘  └───────┘ └─┘   └┘  └───┘└───────┘  └────┘ └─
pid        └┘           └─┘        └──────────┘       
st     └─────────────────────────────────┘└───────┘└┘└─────────
445  
src  
typ  
doc  
txt  
par  
pid  
st   
446  @[simp] lemma support_zero : (0 : Π₀ i, β i).support = ∅ := rfl
id                                     └┘    └─────┘       └─┘
src                                    └┘       └─────┘       └─┘
typ                                    └┘    └─────┘       └─┘
doc    └──┘
447  
448  @[simp] lemma mem_support_iff (f : Π₀ i, β i) : ∀i:ι, i ∈ f.support ↔ f i ≠ 0 :=
id                                      └┘              └──────┘    
src                                     └┘                    └──────┘      
typ                                     └┘              └──────┘    
doc    └──┘
449  f.mem_support_to_fun
id   └─────────────────┘
src   └─────────────────┘
typ  └─────────────────┘
450  
451  @[simp] lemma support_eq_empty {f : Π₀ i, β i} : f.support = ∅ ↔ f = 0 :=
id                                       └┘       └──────┘     
src                                      └┘           └──────┘      
typ                                      └┘       └──────┘     
doc    └──┘
452  ⟨λ H, ext $ by simpa [finset.ext] using H, by simp {contextual:=tt}⟩
id        └─┘             └────────┘                               └┘
src        └─┘      └─────┘└────────┘└──────┘      └───┘ └──────────┘└┘
typ       └─┘      └─────┘└────────┘└──────┘     └───┘ └──────────┘└┘
doc                 └─────┘          └──────┘      └───┘ └──────────┘  
txt                 └─────┘          └──────┘      └───┘ └──────────┘  
par                 └─────┘          └──────┘      └───┘ └──────────┘  
pid                                └────┘           └──────────┘  
st                 └─────────────────────────┘    └────────────────────┘
453  
454  instance decidable_zero : decidable_pred (eq (0 : Π₀ i, β i)) :=
id                             └────────────┘  └┘      └┘   
src                            └────────────┘  └┘      └┘  
typ                            └────────────┘  └┘      └┘   
455  λ f, decidable_of_iff _ $ support_eq_empty.trans eq_comm
id       └──────────────┘     └──────────────┘└────┘ └─────┘
src       └──────────────┘     └──────────────┘└────┘ └─────┘
typ      └──────────────┘     └──────────────┘└────┘ └─────┘
456  
457  lemma support_subset_iff {s : set ι} {f : Π₀ i, β i} :
id                                 └─┘        └┘   
src                                └─┘         └┘  
typ                                └─┘        └┘   
458    ↑f.support ⊆ s ↔ (∀i∉s, f i = 0) :=
id     └──────┘           
src     └──────┘               
typ    └──────┘           
459  by simp [set.subset_def];
id            └────────────┘
src     └────┘└────────────┘
typ     └────┘└────────────┘
doc     └────┘              
txt     └────┘              
par     └────┘              
pid                       
st     └───────────────────────
460     exact forall_congr (assume i, @not_imp_comm _ _ (classical.dec _) (classical.dec _))
id            └──────────┘             └──────────┘                        └───────────┘
src     └────┘└──────────┘       └──┘ └──────────┘└───┘              └──┘ └───────────┘└────
typ     └────┘└──────────┘       └──┘ └──────────┘└───┘              └──┘ └───────────┘└────
doc     └────┘                   └──┘             └───┘              └──┘              └────
txt     └────┘                   └──┘             └───┘              └──┘              └────
par     └────┘                   └──┘             └───┘              └──┘              └────
pid                             └──┘             └───┘              └──┘              └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────
461  
src  
typ  
doc  
txt  
par  
pid  
st   
462  lemma support_single_ne_zero {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = {i} :=
id                                                             └────┘   └─────┘   
src                                                                └────┘     └─────┘   
typ                                                            └────┘   └─────┘   
463  begin
st   └─────
464    ext j, by_cases h : i = j,
id                           
src    └───┘  └───────┘ └─┘ 
typ    └───┘  └───────┘ └─┘
doc    └───┘  └───────┘ └─┘  
txt    └───┘  └───────┘ └─┘  
par    └───┘  └───────┘ └─┘  
pid       └┘           └─┘  
st   ──────┘└──────────────────┘└─
465    { subst h, simp [hb] },
id                     └┘
src      └────┘   └────┘  └┘
typ      └────┘  └────┘└┘└┘
doc      └────┘   └────┘  └┘
txt      └────┘   └────┘  └┘
par      └────┘   └────┘  └┘
pid                    
st   ───┘└─────┘└──────────┘└┘
466    simp [ne.symm h, h]
id           └─────┘   
src    └────┘└─────┘ └┘ └┘
typ    └────┘└─────┘└┘└┘
doc    └────┘        └┘ └┘
txt    └────┘        └┘ └┘
par    └────┘        └┘ └┘
pid                └┘ 
st   ─────────────────────┘
467  end
st   └─┘
468  
469  lemma support_single_subset {i : ι} {b : β i} : (single i b).support ⊆ {i} :=
id                                                 └────┘   └─────┘   
src                                                   └────┘     └─────┘   
typ                                                └────┘   └─────┘   
470  support_mk_subset
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
471  
472  section map_range_and_zip_with
473  
474  variables {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
475  variables [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]
id                  └──────┘             └──────┘     
src                  └──────┘               └──────┘
typ                 └──────┘             └──────┘     
476  variables [Π i, decidable_pred (eq (0 : β₁ i))] [Π i, decidable_pred (eq (0 : β₂ i))]
id                  └────────────┘  └┘                  └────────────┘  └┘         
src                  └────────────┘  └┘                    └────────────┘  └┘
typ                 └────────────┘  └┘                  └────────────┘  └┘         
477  
478  lemma map_range_def {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
id                                └┘    └┘                          └┘  └┘ 
src                                                                       └┘  
typ                               └┘    └┘                          └┘  └┘ 
479    map_range f hf g = mk g.support (λ i, f i.1 (g i.1)) :=
id     └───────┘  └┘   └┘ └──────┘           
src    └───────┘         └┘  └──────┘                
typ    └───────┘  └┘   └┘ └──────┘           
doc    └───────┘
480  begin
st   └─────
481    ext i,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
482    by_cases h : g i = 0,
id                    
src    └───────┘ └─┘  └┘
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘   └┘
txt    └───────┘ └─┘   └┘
par    └───────┘ └─┘   └┘
pid             └─┘   
st   ─────────────────────┘└─
483    { simp [h, hf] },
id               └┘
src      └────┘ └┘  └┘
typ      └────┘└┘└┘└┘
doc      └────┘ └┘  └┘
txt      └────┘ └┘  └┘
par      └────┘ └┘  └┘
pid           └┘  
st   ───┘└───────────┘└┘
484    { simp at h, simp [h, hf] }
id                          └┘
src      └───────┘  └────┘ └┘  └┘
typ      └───────┘  └────┘└┘└┘└┘
doc      └───────┘  └────┘ └┘  └┘
txt      └───────┘  └────┘ └┘  └┘
par      └───────┘  └────┘ └┘  └┘
pid          └──┘       └┘  
st   ────────────┘└─────────────┘└─
485  end
st   ──┘
486  
487  lemma support_map_range {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
id                                    └┘    └┘                          └┘  └┘ 
src                                                                           └┘  
typ                                   └┘    └┘                          └┘  └┘ 
488    (map_range f hf g).support ⊆ g.support :=
id      └───────┘  └┘  └─────┘   └──────┘
src     └───────┘        └─────┘    └──────┘
typ     └───────┘  └┘  └─────┘   └──────┘
doc     └───────┘
489  by simp [map_range_def]
id            └───────────┘
src     └────┘└───────────┘└─
typ     └────┘└───────────┘└─
doc     └────┘             └─
txt     └────┘             └─
par     └────┘             └─
pid                      
st     └─────────────────────
490  
src  
typ  
doc  
txt  
par  
pid  
st   
491  @[simp] lemma map_range_single {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {i : ι} {b : β₁ i} :
id                                           └┘    └┘                                 └┘ 
src                                                                         
typ                                          └┘    └┘                                 └┘ 
doc    └──┘
492    map_range f hf (single i b) = single i (f i b) :=
id     └───────┘  └┘  └────┘     └────┘     
src    └───────┘       └────┘       └────┘
typ    └───────┘  └┘  └────┘     └────┘     
doc    └───────┘
493  dfinsupp.ext $ λ i', by by_cases i = i'; [{subst i', simp}, simp [h, hf]]
id   └──────────┘     └┘                └┘         └┘                 └┘
src  └──────────┘            └───────┘      └────┘    └──┘   └────┘ └┘  
typ  └──────────┘     └┘     └───────┘└┘   └────┘└┘  └──┘   └────┘└┘└┘
doc                          └───────┘        └────┘    └──┘   └────┘ └┘  
txt                          └───────┘        └────┘    └──┘   └────┘ └┘  
par                          └───────┘        └────┘    └──┘   └────┘ └┘  
pid                                                               └┘  
st                          └─────────────────┘└───────┘└────┘└┘└────────────┘
494  
495  lemma zip_with_def {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :
id                               └┘    └┘                                 └┘  └┘         └┘  └┘ 
src                                                                               └┘               └┘  
typ                              └┘    └┘                                 └┘  └┘         └┘  └┘ 
496    zip_with f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) (λ i, f i.1 (g₁ i.1) (g₂ i.1)) :=
id     └──────┘  └┘ └┘ └┘  └┘  └┘└──────┘  └┘└──────┘           └┘     └┘ 
src    └──────┘             └┘    └──────┘    └──────┘                          
typ    └──────┘  └┘ └┘ └┘  └┘  └┘└──────┘  └┘└──────┘           └┘     └┘ 
497  begin
st   └─────
498    ext i,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
499    by_cases h1 : g₁ i = 0; by_cases h2 : g₂ i = 0;
id                   └┘                    └┘ 
src    └───────┘  └─┘   └┘  └───────┘  └─┘    └┘
typ    └───────┘  └─┘└┘└┘  └───────┘  └─┘└┘ └┘
doc    └───────┘  └─┘    └┘  └───────┘  └─┘    └┘
txt    └───────┘  └─┘    └┘  └───────┘  └─┘    └┘
par    └───────┘  └─┘    └┘  └───────┘  └─┘    └┘
pid              └─┘                └─┘    
st   ──────────────────────────────────────────────────
500    try {simp at h1 h2}; simp [h1, h2, hf]
id                                └┘  └┘  └┘
src    └───┘└───────────┘  └────┘  └┘  └┘  └┘
typ    └───┘└───────────┘  └────┘└┘└┘└┘└┘└┘└┘
doc    └───┘└───────────┘  └────┘  └┘  └┘  └┘
txt    └───┘└───────────┘  └────┘  └┘  └┘  └┘
par    └───┘└───────────┘  └────┘  └┘  └┘  └┘
pid       └──────────────┘        └┘  └┘  
st   ──────┘└───────────┘└┘└─────────────────┘
501  end
st   └─┘
502  
503  lemma support_zip_with {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :
id                                   └┘    └┘                                 └┘  └┘         └┘  └┘ 
src                                                                                   └┘               └┘  
typ                                  └┘    └┘                                 └┘  └┘         └┘  └┘ 
504    (zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=
id      └──────┘  └┘ └┘ └┘ └─────┘   └┘└──────┘  └┘└──────┘
src     └──────┘            └─────┘     └──────┘    └──────┘
typ     └──────┘  └┘ └┘ └┘ └─────┘   └┘└──────┘  └┘└──────┘
505  by simp [zip_with_def]
id            └──────────┘
src     └────┘└──────────┘└─
typ     └────┘└──────────┘└─
doc     └────┘            └─
txt     └────┘            └─
par     └────┘            └─
pid                     
st     └────────────────────
506  
src  
typ  
doc  
txt  
par  
pid  
st   
507  end map_range_and_zip_with
508  
509  lemma erase_def (i : ι) (f : Π₀ i, β i) :
id                               └┘   
src                               └┘  
typ                              └┘   
510    f.erase i = mk (f.support.erase i) (λ j, f j.1) :=
id     └────┘   └┘  └──────┘└────┘         
src     └────┘    └┘   └──────┘└────┘             
typ    └────┘   └┘  └──────┘└────┘         
doc                             └────┘
511  begin
st   └─────
512    ext j,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
513    by_cases h1 : j = i; by_cases h2 : f j = 0;
id                                      
src    └───────┘  └─┘    └───────┘  └─┘   └┘
typ    └───────┘  └─┘  └───────┘  └─┘ └┘
doc    └───────┘  └─┘     └───────┘  └─┘   └┘
txt    └───────┘  └─┘     └───────┘  └─┘   └┘
par    └───────┘  └─┘     └───────┘  └─┘   └┘
pid              └─┘               └─┘   
st   ──────────────────────────────────────────────
514    try {simp at h2}; simp [h1, h2]
id                             └┘  └┘
src    └───┘└────────┘  └────┘  └┘  └┘
typ    └───┘└────────┘  └────┘└┘└┘└┘└┘
doc    └───┘└────────┘  └────┘  └┘  └┘
txt    └───┘└────────┘  └────┘  └┘  └┘
par    └───┘└────────┘  └────┘  └┘  └┘
pid       └───────────┘        └┘  
st   ──────┘└────────┘└┘└─────────────┘
515  end
st   └─┘
516  
517  @[simp] lemma support_erase (i : ι) (f : Π₀ i, β i) :
id                                           └┘   
src                                           └┘  
typ                                          └┘   
doc    └──┘
518    (f.erase i).support = f.support.erase i :=
id      └────┘  └─────┘   └──────┘└────┘ 
src      └────┘   └─────┘    └──────┘└────┘
typ     └────┘  └─────┘   └──────┘└────┘ 
doc                                   └────┘
519  begin
st   └─────
520    ext j,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
521    by_cases h1 : j = i; by_cases h2 : f j = 0;
id                                      
src    └───────┘  └─┘    └───────┘  └─┘   └┘
typ    └───────┘  └─┘  └───────┘  └─┘ └┘
doc    └───────┘  └─┘     └───────┘  └─┘   └┘
txt    └───────┘  └─┘     └───────┘  └─┘   └┘
par    └───────┘  └─┘     └───────┘  └─┘   └┘
pid              └─┘               └─┘   
st   ──────────────────────────────────────────────
522    try {simp at h2}; simp [h1, h2]
id                             └┘  └┘
src    └───┘└────────┘  └────┘  └┘  └┘
typ    └───┘└────────┘  └────┘└┘└┘└┘└┘
doc    └───┘└────────┘  └────┘  └┘  └┘
txt    └───┘└────────┘  └────┘  └┘  └┘
par    └───┘└────────┘  └────┘  └┘  └┘
pid       └───────────┘        └┘  
st   ──────┘└────────┘└┘└─────────────┘
523  end
st   └─┘
524  
525  section filter_and_subtype_domain
526  
527  variables {p : ι → Prop} [decidable_pred p]
id                             └────────────┘
src                            └────────────┘
typ                            └────────────┘
528  
529  lemma filter_def (f : Π₀ i, β i) :
id                         └┘   
src                        └┘  
typ                        └┘   
530    f.filter p = mk (f.support.filter p) (λ i, f i.1) :=
id     └─────┘   └┘  └──────┘└─────┘         
src     └─────┘    └┘   └──────┘└─────┘             
typ    └─────┘   └┘  └──────┘└─────┘         
doc     └─────┘                  └─────┘
531  by ext i; by_cases h1 : p i; by_cases h2 : f i = 0;
id                                              
src     └───┘  └───────┘  └─┘    └───────┘  └─┘  └┘
typ     └───┘  └───────┘  └─┘  └───────┘  └─┘└┘
doc     └───┘  └───────┘  └─┘    └───────┘  └─┘   └┘
txt     └───┘  └───────┘  └─┘    └───────┘  └─┘   └┘
par     └───┘  └───────┘  └─┘    └───────┘  └─┘   └┘
pid        └┘            └─┘              └─┘   
st     └─────────────────────────────────────────────────
532  try {simp at h2}; simp [h1, h2]
id                           └┘  └┘
src  └───┘└────────┘  └────┘  └┘  └─
typ  └───┘└────────┘  └────┘└┘└┘└┘└─
doc  └───┘└────────┘  └────┘  └┘  └─
txt  └───┘└────────┘  └────┘  └┘  └─
par  └───┘└────────┘  └────┘  └┘  └─
pid     └───────────┘        └┘  
st   ────┘└────────┘└┘└──────────────
533  
src  
typ  
doc  
txt  
par  
pid  
st   
534  @[simp] lemma support_filter (f : Π₀ i, β i) :
id                                     └┘   
src                                    └┘  
typ                                    └┘   
doc    └──┘
535    (f.filter p).support = f.support.filter p :=
id      └─────┘  └─────┘   └──────┘└─────┘ 
src      └─────┘   └─────┘    └──────┘└─────┘
typ     └─────┘  └─────┘   └──────┘└─────┘ 
doc      └─────┘                       └─────┘
536  by ext i; by_cases h : p i; simp [h]
id                                   
src     └───┘  └───────┘ └─┘    └────┘ └─
typ     └───┘  └───────┘ └─┘  └────┘└─
doc     └───┘  └───────┘ └─┘    └────┘ └─
txt     └───┘  └───────┘ └─┘    └────┘ └─
par     └───┘  └───────┘ └─┘    └────┘ └─
pid        └┘           └─┘         
st     └──────────────────────────────────
537  
src  
typ  
doc  
txt  
par  
pid  
st   
538  lemma subtype_domain_def (f : Π₀ i, β i) :
id                                 └┘   
src                                └┘  
typ                                └┘   
539    f.subtype_domain p = mk (f.support.subtype p) (λ i, f i.1) :=
id     └─────────────┘   └┘  └──────┘└──────┘         
src     └─────────────┘    └┘   └──────┘└──────┘             
typ    └─────────────┘   └┘  └──────┘└──────┘         
doc     └─────────────┘
540  by ext i; cases i with i hi;
id                   
src     └───┘  └────┘ └────────┘
typ     └───┘  └────┘└────────┘
doc     └───┘  └────┘ └────────┘
txt     └───┘  └────┘ └────────┘
par     └───┘  └────┘ └────────┘
pid        └┘        └────────┘
st     └──────────────────────────
541  by_cases h1 : p i; by_cases h2 : f i = 0;
id                                    
src  └───────┘  └─┘    └───────┘  └─┘  └┘
typ  └───────┘  └─┘  └───────┘  └─┘└┘
doc  └───────┘  └─┘    └───────┘  └─┘   └┘
txt  └───────┘  └─┘    └───────┘  └─┘   └┘
par  └───────┘  └─┘    └───────┘  └─┘   └┘
pid            └─┘              └─┘   
st   ──────────────────────────────────────────
542  try {simp at h2}; dsimp; simp [h1, h2]
id                                  └┘  └┘
src  └───┘└────────┘  └───┘  └────┘  └┘  └─
typ  └───┘└────────┘  └───┘  └────┘└┘└┘└┘└─
doc  └───┘└────────┘  └───┘  └────┘  └┘  └─
txt  └───┘└────────┘  └───┘  └────┘  └┘  └─
par  └───┘└────────┘  └───┘  └────┘  └┘  └─
pid     └───────────┘               └┘  
st   ────┘└────────┘└┘└─────────────────────
543  
src  
typ  
doc  
txt  
par  
pid  
st   
544  @[simp] lemma support_subtype_domain {f : Π₀ i, β i} :
id                                             └┘   
src                                            └┘  
typ                                            └┘   
doc    └──┘
545    (subtype_domain p f).support = f.support.subtype p :=
id      └────────────┘   └─────┘   └──────┘└──────┘ 
src     └────────────┘     └─────┘    └──────┘└──────┘
typ     └────────────┘   └─────┘   └──────┘└──────┘ 
doc     └────────────┘
546  by ext i; cases i with i hi;
id                   
src     └───┘  └────┘ └────────┘
typ     └───┘  └────┘└────────┘
doc     └───┘  └────┘ └────────┘
txt     └───┘  └────┘ └────────┘
par     └───┘  └────┘ └────────┘
pid        └┘        └────────┘
st     └──────────────────────────
547  by_cases h1 : p i; by_cases h2 : f i = 0;
id                                    
src  └───────┘  └─┘    └───────┘  └─┘  └┘
typ  └───────┘  └─┘  └───────┘  └─┘└┘
doc  └───────┘  └─┘    └───────┘  └─┘   └┘
txt  └───────┘  └─┘    └───────┘  └─┘   └┘
par  └───────┘  └─┘    └───────┘  └─┘   └┘
pid            └─┘              └─┘   
st   ──────────────────────────────────────────
548  try {simp at h2}; dsimp; simp [h1, h2]
id                                  └┘  └┘
src  └───┘└────────┘  └───┘  └────┘  └┘  └─
typ  └───┘└────────┘  └───┘  └────┘└┘└┘└┘└─
doc  └───┘└────────┘  └───┘  └────┘  └┘  └─
txt  └───┘└────────┘  └───┘  └────┘  └┘  └─
par  └───┘└────────┘  └───┘  └────┘  └┘  └─
pid     └───────────┘               └┘  
st   ────┘└────────┘└┘└─────────────────────
549  
src  
typ  
doc  
txt  
par  
pid  
st   
550  end filter_and_subtype_domain
551  
552  end support_basic
553  
554  lemma support_add [Π i, add_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] {g₁ g₂ : Π₀ i, β i} :
id                          └────────┘           └────────────┘  └┘                    └┘   
src                          └────────┘              └────────────┘  └┘                      └┘  
typ                         └────────┘           └────────────┘  └┘                    └┘   
555    (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
id      └┘  └┘ └─────┘   └┘└──────┘  └┘└──────┘
src            └─────┘     └──────┘    └──────┘
typ     └┘  └┘ └─────┘   └┘└──────┘  └┘└──────┘
556  support_zip_with
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
557  
558  @[simp] lemma support_neg [Π i, add_group (β i)] [Π i, decidable_pred (eq (0 : β i))] {f : Π₀ i, β i} :
id                                  └───────┘           └────────────┘  └┘                └┘   
src                                  └───────┘              └────────────┘  └┘                  └┘  
typ                                 └───────┘           └────────────┘  └┘                └┘   
doc    └──┘
559    support (-f) = support f :=
id     └─────┘     └─────┘ 
src    └─────┘      └─────┘
typ    └─────┘     └─────┘ 
560  by ext i; simp
src     └───┘  └────
typ     └───┘  └────
doc     └───┘  └────
txt     └───┘  └────
par     └───┘  └────
pid        └┘      
st     └────────────
561  
src  
typ  
doc  
txt  
par  
pid  
st   
562  local attribute [instance] dfinsupp.to_module
id                              └────────────────┘
src                             └────────────────┘
typ                             └────────────────┘
563  
564  lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
id                                    └──┘        └────────────┘           └────┘    
src                                   └──┘          └────────────┘              └────┘
typ                                   └──┘        └────────────┘           └────┘    
doc                                                                             └────┘
565    [Π (i : ι), decidable_pred (eq (0 : β i))]
id                └────────────┘  └┘       
src                └────────────┘  └┘
typ               └────────────┘  └┘       
566    {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support :=
id                 └┘           └─────┘   └──────┘
src                 └┘                └─────┘    └──────┘
typ                └┘           └─────┘   └──────┘
567  λ x, by simp [dfinsupp.mem_support_iff, not_imp_not] {contextual := tt}
id                └──────────────────────┘  └─────────┘                 └┘
src          └────┘└──────────────────────┘└┘└─────────┘└┘ └────────────┘└┘└─
typ         └────┘└──────────────────────┘└┘└─────────┘└┘ └────────────┘└┘└─
doc          └────┘                        └┘           └┘ └────────────┘  └─
txt          └────┘                        └┘           └┘ └────────────┘  └─
par          └────┘                        └┘           └┘ └────────────┘  └─
pid                                      └┘            └────────────┘  
st          └────────────────────────────────────────────────────────────────
568  
src  
typ  
doc  
txt  
par  
pid  
st   
569  instance [decidable_eq ι] [Π i, has_zero (β i)] [Π i, decidable_eq (β i)] : decidable_eq (Π₀ i, β i) :=
id             └──────────┘        └──────┘           └──────────┘        └──────────┘  └┘   
src            └──────────┘          └──────┘              └──────────┘          └──────────┘  └┘  
typ            └──────────┘        └──────┘           └──────────┘        └──────────┘  └┘   
570  assume f g, decidable_of_iff (f.support = g.support ∧ (∀i∈f.support, f i = g i))
id             └──────────────┘  └──────┘  └──────┘     └──────┘      
src              └──────────────┘   └──────┘   └──────┘       └──────┘      
typ            └──────────────┘  └──────┘  └──────┘     └──────┘      
571    ⟨assume ⟨h₁, h₂⟩, ext $ assume i,
id                 └┘   └─┘          
src                      └─┘
typ                └┘   └─┘          
572        if h : i ∈ f.support then h₂ i h else
id         └┘       └──────┘          
src        └┘         └──────┘
typ        └┘       └──────┘          
573          have hf : f i = 0, by rwa [f.mem_support_iff, not_not] at h,
id           └──┘                                       └─────┘
src                               └───┘                 └┘└─────┘└────┘
typ          └──┘               └───┘└───────────────┘└┘└─────┘└────┘
doc                                └───┘                 └┘       └────┘
txt                                └───┘                 └┘       └────┘
par                                └───┘                 └┘       └────┘
pid                                   └┘                 └┘       └───┘
st                                └─────────────────────┘└───────┘└───┘
574          have hg : g i = 0, by rwa [h₁, g.mem_support_iff, not_not] at h,
id                                   └┘                     └─────┘
src                               └───┘  └┘                 └┘└─────┘└────┘
typ                             └───┘└┘└┘└───────────────┘└┘└─────┘└────┘
doc                                └───┘  └┘                 └┘       └────┘
txt                                └───┘  └┘                 └┘       └────┘
par                                └───┘  └┘                 └┘       └────┘
pid                                   └┘  └┘                 └┘       └───┘
st                                └──────┘└─────────────────┘└───────┘└───┘
575          by rw [hf, hg],
id                  └┘  └┘
src             └──┘  └┘  
typ             └──┘└┘└┘└┘
doc             └──┘  └┘  
txt             └──┘  └┘  
par             └──┘  └┘  
pid               └┘  └┘  
st             └─────┘└──┘
576      by intro h; subst h; simp⟩
id                         
src         └─────┘  └────┘   └──┘
typ         └─────┘  └────┘  └──┘
doc         └─────┘  └────┘   └──┘
txt         └─────┘  └────┘   └──┘
par         └─────┘  └────┘   └──┘
pid              └┘       
st         └─────────────────────┘
577  
578  section prod_and_sum
579  
580  variables {γ : Type w}
581  
582  -- [to_additive sum] for dfinsupp.prod doesn't work, the equation lemmas are not generated
583  /-- `sum f g` is the sum of `g i (f i)` over the support of `f`. -/
584  def sum [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [add_comm_monoid γ]
id                └──────┘           └────────────┘  └┘            └─────────────┘ 
src                └──────┘              └────────────┘  └┘              └─────────────┘
typ               └──────┘           └────────────┘  └┘            └─────────────┘ 
585    (f : Π₀ i, β i) (g : Π i, β i → γ) : γ :=
id          └┘                      
src         └┘  
typ         └┘                      
586  f.support.sum (λi, g i (f i))
id   └──────┘└──┘         
src   └──────┘└──┘
typ  └──────┘└──┘         
587  
588  /-- `prod f g` is the product of `g i (f i)` over the support of `f`. -/
589  @[to_additive]
doc    └─────────┘
590  def prod [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id                 └──────┘           └────────────┘  └┘            └─────────┘ 
src                 └──────┘              └────────────┘  └┘              └─────────┘
typ                └──────┘           └────────────┘  └┘            └─────────┘ 
591    (f : Π₀ i, β i) (g : Π i, β i → γ) : γ :=
id          └┘                      
src         └┘  
typ         └┘                      
592  f.support.prod (λi, g i (f i))
id   └──────┘└───┘         
src   └──────┘└───┘
typ  └──────┘└───┘         
doc           └───┘
593  
594  @[to_additive]
doc    └─────────┘
595  lemma prod_map_range_index {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
id                                                      
typ                                                     
596    [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]
id          └──────┘  └┘         └──────┘  └┘ 
src          └──────┘               └──────┘
typ         └──────┘  └┘         └──────┘  └┘ 
597    [Π i, decidable_pred (eq (0 : β₁ i))] [Π i, decidable_pred (eq (0 : β₂ i))] [comm_monoid γ]
id          └────────────┘  └┘      └┘          └────────────┘  └┘      └┘      └─────────┘ 
src          └────────────┘  └┘                    └────────────┘  └┘               └─────────┘
typ         └────────────┘  └┘      └┘          └────────────┘  └┘      └┘      └─────────┘ 
598    {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} {h : Π i, β₂ i → γ} (h0 : ∀i, h i 0 = 1) :
id              └┘    └┘                          └┘  └┘            └┘                   
src                                                     └┘                                             
typ             └┘    └┘                          └┘  └┘            └┘                   
599    (map_range f hf g).prod h = g.prod (λi b, h i (f i b)) :=
id      └───────┘  └┘  └──┘    └───┘           
src     └───────┘        └──┘      └───┘
typ     └───────┘  └┘  └──┘    └───┘           
doc     └───────┘        └──┘       └───┘
600  begin
st   └─────
601    rw [map_range_def],
id         └───────────┘
src    └──┘└───────────┘
typ    └──┘└───────────┘
doc    └──┘             
txt    └──┘             
par    └──┘             
pid      └┘             
st   ──────────────────┘└──
602    refine (finset.prod_subset support_mk_subset _).trans _,
id             └────────────────┘ └───────────────┘
src    └─────┘ └────────────────┘└───────────────┘└─────────┘
typ    └─────┘ └────────────────┘└───────────────┘└─────────┘
doc    └─────┘                                    └─────────┘
txt    └─────┘                                    └─────────┘
par    └─────┘                                    └─────────┘
pid                                              └─────────┘
st   ────────────────────────────────────────────────────────┘└─
603    { intros i h1 h2,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
604      dsimp, simp [h1] at h2, dsimp at h2,
id                    └┘
src      └───┘  └────┘  └─────┘  └─────────┘
typ      └───┘  └────┘└┘└─────┘  └─────────┘
doc      └───┘  └────┘  └─────┘  └─────────┘
txt      └───┘  └────┘  └─────┘  └─────────┘
par      └───┘  └────┘  └─────┘  └─────────┘
pid                   └───┘       └───┘
st   ────────┘└───────────────┘└───────────┘└─
605      simp [h1, h2, h0] },
id             └┘  └┘  └┘
src      └────┘  └┘  └┘  └┘
typ      └────┘└┘└┘└┘└┘└┘└┘
doc      └────┘  └┘  └┘  └┘
txt      └────┘  └┘  └┘  └┘
par      └────┘  └┘  └┘  └┘
pid            └┘  └┘  
st   ─────────────────────┘└┘
606    { refine finset.prod_congr rfl _,
id              └───────────────┘ └─┘
src      └─────┘└───────────────┘└─┘└┘
typ      └─────┘└───────────────┘└─┘└┘
doc      └─────┘                    └┘
txt      └─────┘                    └┘
par      └─────┘                    └┘
pid                                └┘
st   ─────────────────────────────────┘└─
607      intros i h1,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
608      simp [h1] }
id             └┘
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid            
st   ─────────────┘└─
609  end
st   ──┘
610  
611  @[to_additive]
doc    └─────────┘
612  lemma prod_zero_index [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id                              └─────────────┘           └────────────┘  └┘            └─────────┘ 
src                              └─────────────┘              └────────────┘  └┘              └─────────┘
typ                             └─────────────┘           └────────────┘  └┘            └─────────┘ 
613    {h : Π i, β i → γ} : (0 : Π₀ i, β i).prod h = 1 :=
id                           └┘    └──┘   
src                              └┘       └──┘    
typ                          └┘    └──┘   
doc                                        └──┘
614  rfl
id   └─┘
src  └─┘
typ  └─┘
615  
616  @[to_additive]
doc    └─────────┘
617  lemma prod_single_index [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id                                └──────┘           └────────────┘  └┘            └─────────┘ 
src                                └──────┘              └────────────┘  └┘              └─────────┘
typ                               └──────┘           └────────────┘  └┘            └─────────┘ 
618    {i : ι} {b : β i} {h : Π i, β i → γ} (h_zero : h i 0 = 1) :
id                                                 
src                                                         
typ                                                
619    (single i b).prod h = h i b :=
id      └────┘   └──┘      
src     └────┘     └──┘    
typ     └────┘   └──┘      
doc                └──┘
620  begin
st   └─────
621    by_cases h : b = 0,
id                   
src    └───────┘ └─┘ └┘
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  └┘
txt    └───────┘ └─┘  └┘
par    └───────┘ └─┘  └┘
pid             └─┘  
st   ───────────────────┘└─
622    { simp [h, prod_zero_index, h_zero], refl },
id               └─────────────┘  └────┘
src      └────┘ └┘└─────────────┘└┘        └───┘
typ      └────┘└┘└─────────────┘└┘└────┘  └───┘
doc      └────┘ └┘               └┘        └───┘
txt      └────┘ └┘               └┘        └───┘
par      └────┘ └┘               └┘        └───┘
pid           └┘               └┘            
st   ───┘└───────────────────────────────┘└─────┘└┘
623    { simp [dfinsupp.prod, support_single_ne_zero h] }
id             └───────────┘  └────────────────────┘ 
src      └────┘└───────────┘└┘└────────────────────┘ └┘
typ      └────┘└───────────┘└┘└────────────────────┘└┘
doc      └────┘└───────────┘└┘                       └┘
txt      └────┘             └┘                       └┘
par      └────┘             └┘                       └┘
pid                       └┘                       
st   ──────────────────────────────────────────────────┘└─
624  end
st   ──┘
625  
626  @[to_additive]
doc    └─────────┘
627  lemma prod_neg_index [Π i, add_group (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id                             └───────┘           └────────────┘  └┘            └─────────┘ 
src                             └───────┘              └────────────┘  └┘              └─────────┘
typ                            └───────┘           └────────────┘  └┘            └─────────┘ 
628    {g : Π₀ i, β i} {h : Π i, β i → γ} (h0 : ∀i, h i 0 = 1) :
id          └┘                                 
src         └┘                                           
typ         └┘                                 
629    (-g).prod h = g.prod (λi b, h i (- b)) :=
id       └──┘    └───┘          
src       └──┘      └───┘             
typ      └──┘    └───┘          
doc        └──┘       └───┘
630  prod_map_range_index h0
id   └──────────────────┘ └┘
src  └──────────────────┘
typ  └──────────────────┘ └┘
631  
632  @[simp] lemma sum_apply {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁}
id                                           └──────────┘ └┘        └┘
src                                          └──────────┘
typ                                          └──────────┘ └┘        └┘
doc    └──┘
633    [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))]
id        └┘  └──────┘  └┘ └┘        └────────────┘  └┘      └┘ 
src           └──────┘                └────────────┘  └┘
typ       └┘  └──────┘  └┘ └┘        └────────────┘  └┘      └┘ 
634    [Π i, add_comm_monoid (β i)]
id          └─────────────┘   
src          └─────────────┘
typ         └─────────────┘   
635    {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i} {i₂ : ι} :
id          └┘ └┘ └┘ └┘         └┘  └┘ └┘   └┘           
src         └┘                              └┘  
typ         └┘ └┘ └┘ └┘         └┘  └┘ └┘   └┘           
636    (f.sum g) i₂ = f.sum (λi₁ b, g i₁ b i₂) :=
id      └──┘   └┘  └──┘   └┘    └┘  └┘
src      └──┘         └──┘
typ     └──┘   └┘  └──┘   └┘    └┘  └┘
doc      └──┘          └──┘
637  (f.support.sum_hom (λf : Π₀ i, β i, f i₂)).symm
id    └──────┘└──────┘       └┘      └┘  └──┘
src    └──────┘└──────┘       └┘              └──┘
typ   └──────┘└──────┘       └┘      └┘  └──┘
638  
639  lemma support_sum {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁}
id                                     └──────────┘ └┘        └┘
src                                    └──────────┘
typ                                    └──────────┘ └┘        └┘
640    [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))]
id        └┘  └──────┘  └┘ └┘        └────────────┘  └┘      └┘ 
src           └──────┘                └────────────┘  └┘
typ       └┘  └──────┘  └┘ └┘        └────────────┘  └┘      └┘ 
641    [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id          └─────────────┘           └────────────┘  └┘       
src          └─────────────┘              └────────────┘  └┘
typ         └─────────────┘           └────────────┘  └┘       
642    {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i} :
id          └┘ └┘ └┘ └┘         └┘  └┘ └┘   └┘   
src         └┘                              └┘  
typ         └┘ └┘ └┘ └┘         └┘  └┘ └┘   └┘   
643    (f.sum g).support ⊆ f.support.bind (λi, (g i (f i)).support) :=
id      └──┘  └─────┘   └──────┘└───┘            └─────┘
src      └──┘   └─────┘    └──────┘└───┘                 └─────┘
typ     └──┘  └─────┘   └──────┘└───┘            └─────┘
doc      └──┘                       └───┘
644  have ∀i₁ : ι, f.sum (λ (i : ι₁) (b : β₁ i), (g i b) i₁) ≠ 0 →
id                └──┘         └┘       └┘         └┘  
src                 └──┘                                     
typ               └──┘         └┘       └┘         └┘  
doc                 └──┘
645      (∃ (i : ι₁), f i ≠ 0 ∧ ¬ (g i (f i)) i₁ = 0),
id              └┘                 └┘ 
src                                         
typ             └┘                 └┘ 
646    from assume i₁ h,
id                 └┘ 
typ                └┘ 
647    let ⟨i, hi, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
id     └─┘    └┘  └┘     └──────────────────────────────────┘ 
src                └┘     └──────────────────────────────────┘
typ    └─┘    └┘  └┘     └──────────────────────────────────┘ 
648    ⟨i, (f.mem_support_iff i).mp hi, ne⟩,
id          └──────────────┘   └┘
src          └──────────────┘   └┘
typ         └──────────────┘   └┘
649  by simpa [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply] using this
id             └───────────────┘  └─────────────┘  └─────────────┘  └───────┘        └──┘
src     └─────┘└───────────────┘└┘└─────────────┘└┘└─────────────┘└┘└───────┘└──────┘    
typ     └─────┘└───────────────┘└┘└─────────────┘└┘└─────────────┘└┘└───────┘└──────┘└──┘
doc     └─────┘                 └┘               └┘               └┘         └──────┘    
txt     └─────┘                 └┘               └┘               └┘         └──────┘    
par     └─────┘                 └┘               └┘               └┘         └──────┘    
pid                           └┘               └┘               └┘         └────┘    
st     └──────────────────────────────────────────────────────────────────────────────────
650  
src  
typ  
doc  
txt  
par  
pid  
st   
651  @[simp] lemma sum_zero [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                               └─────────────┘           └────────────┘  └┘       
src                               └─────────────┘              └────────────┘  └┘
typ                              └─────────────┘           └────────────┘  └┘       
doc    └──┘
652    [add_comm_monoid γ] {f : Π₀ i, β i} :
id      └─────────────┘        └┘   
src     └─────────────┘         └┘  
typ     └─────────────┘        └┘   
653    f.sum (λi b, (0 : γ)) = 0 :=
id     └──┘              
src     └──┘                 
typ    └──┘              
doc     └──┘
654  finset.sum_const_zero
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
655  
656  @[simp] lemma sum_add [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                              └─────────────┘           └────────────┘  └┘       
src                              └─────────────┘              └────────────┘  └┘
typ                             └─────────────┘           └────────────┘  └┘       
doc    └──┘
657    [add_comm_monoid γ] {f : Π₀ i, β i} {h₁ h₂ : Π i, β i → γ} :
id      └─────────────┘        └┘                      
src     └─────────────┘         └┘  
typ     └─────────────┘        └┘                      
658    f.sum (λi b, h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂ :=
id     └──┘      └┘    └┘     └──┘ └┘  └──┘ └┘
src     └──┘                          └──┘      └──┘
typ    └──┘      └┘    └┘     └──┘ └┘  └──┘ └┘
doc     └──┘                            └──┘       └──┘
659  finset.sum_add_distrib
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
660  
661  @[simp] lemma sum_neg [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                              └─────────────┘           └────────────┘  └┘       
src                              └─────────────┘              └────────────┘  └┘
typ                             └─────────────┘           └────────────┘  └┘       
doc    └──┘
662    [add_comm_group γ] {f : Π₀ i, β i} {h : Π i, β i → γ} :
id      └────────────┘        └┘                  
src     └────────────┘         └┘  
typ     └────────────┘        └┘                  
663    f.sum (λi b, - h i b) = - f.sum h :=
id     └──┘             └──┘ 
src     └──┘                   └──┘
typ    └──┘             └──┘ 
doc     └──┘                      └──┘
664  f.support.sum_hom (@has_neg.neg γ _)
id   └──────┘└──────┘   └─────────┘ 
src   └──────┘└──────┘   └─────────┘
typ  └──────┘└──────┘   └─────────┘ 
665  
666  @[to_additive]
doc    └─────────┘
667  lemma prod_add_index [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                             └─────────────┘           └────────────┘  └┘       
src                             └─────────────┘              └────────────┘  └┘
typ                            └─────────────┘           └────────────┘  └┘       
668    [comm_monoid γ] {f g : Π₀ i, β i}
id      └─────────┘          └┘   
src     └─────────┘           └┘  
typ     └─────────┘          └┘   
669    {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
id                                                    └┘ └┘     └┘  └┘     └┘    └┘
src                                                                                       
typ                                                   └┘ └┘     └┘  └┘     └┘    └┘
670    (f + g).prod h = f.prod h * g.prod h :=
id         └──┘    └───┘   └───┘ 
src          └──┘      └───┘     └───┘
typ        └──┘    └───┘   └───┘ 
doc           └──┘       └───┘      └───┘
671  have f_eq : (f.support ∪ g.support).prod (λi, h i (f i)) = f.prod h,
id                └──────┘  └──────┘ └──┘              └───┘ 
src                └──────┘   └──────┘ └──┘                    └───┘
typ               └──────┘  └──────┘ └──┘              └───┘ 
doc                                     └──┘                     └───┘
672    from (finset.prod_subset (finset.subset_union_left _ _) $
id           └────────────────┘  └──────────────────────┘
src          └────────────────┘  └──────────────────────┘
typ          └────────────────┘  └──────────────────────┘
673      by simp [mem_support_iff, h_zero] {contextual := tt}).symm,
id                └─────────────┘  └────┘                 └┘  └──┘
src         └────┘└─────────────┘└┘      └┘ └────────────┘└┘ └──┘
typ         └────┘└─────────────┘└┘└────┘└┘ └────────────┘└┘ └──┘
doc         └────┘               └┘      └┘ └────────────┘  
txt         └────┘               └┘      └┘ └────────────┘  
par         └────┘               └┘      └┘ └────────────┘  
pid                            └┘       └────────────┘  
st         └────────────────────────────────────────────────┘
674  have g_eq : (f.support ∪ g.support).prod (λi, h i (g i)) = g.prod h,
id                └──────┘  └──────┘ └──┘              └───┘ 
src                └──────┘   └──────┘ └──┘                    └───┘
typ               └──────┘  └──────┘ └──┘              └───┘ 
doc                                     └──┘                     └───┘
675    from (finset.prod_subset (finset.subset_union_right _ _) $
id           └────────────────┘  └───────────────────────┘
src          └────────────────┘  └───────────────────────┘
typ          └────────────────┘  └───────────────────────┘
676      by simp [mem_support_iff, h_zero] {contextual := tt}).symm,
id                └─────────────┘  └────┘                 └┘  └──┘
src         └────┘└─────────────┘└┘      └┘ └────────────┘└┘ └──┘
typ         └────┘└─────────────┘└┘└────┘└┘ └────────────┘└┘ └──┘
doc         └────┘               └┘      └┘ └────────────┘  
txt         └────┘               └┘      └┘ └────────────┘  
par         └────┘               └┘      └┘ └────────────┘  
pid                            └┘       └────────────┘  
st         └────────────────────────────────────────────────┘
677  calc (f + g).support.prod (λi, h i ((f + g) i)) =
id            └─────┘ └──┘              
src             └─────┘ └──┘               
typ           └─────┘ └──┘              
doc                      └──┘
678        (f.support ∪ g.support).prod (λi, h i ((f + g) i)) :
id          └──────┘  └──────┘ └──┘              
src          └──────┘   └──────┘ └──┘               
typ         └──────┘  └──────┘ └──┘              
doc                               └──┘
679      finset.prod_subset support_add $
id       └────────────────┘ └─────────┘
src      └────────────────┘ └─────────┘
typ      └────────────────┘ └─────────┘
680        by simp [mem_support_iff, h_zero] {contextual := tt}
id                  └─────────────┘  └────┘                 └┘
src           └────┘└─────────────┘└┘      └┘ └────────────┘└┘└─
typ           └────┘└─────────────┘└┘└────┘└┘ └────────────┘└┘└─
doc           └────┘               └┘      └┘ └────────────┘  └─
txt           └────┘               └┘      └┘ └────────────┘  └─
par           └────┘               └┘      └┘ └────────────┘  └─
pid                              └┘       └────────────┘  
st           └──────────────────────────────────────────────────
681    ... = (f.support ∪ g.support).prod (λi, h i (f i)) *
id            └──────┘  └──────┘ └──┘             
src  ─┘        └──────┘   └──────┘ └──┘                  
typ  ─┘       └──────┘  └──────┘ └──┘             
doc  ─┘                             └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
682        (f.support ∪ g.support).prod (λi, h i (g i)) :
id          └──────┘  └──────┘ └──┘          
src          └──────┘   └──────┘ └──┘
typ         └──────┘  └──────┘ └──┘          
doc                               └──┘
683      by simp [h_add, finset.prod_mul_distrib]
id                └───┘  └─────────────────────┘
src         └────┘     └┘└─────────────────────┘└─
typ         └────┘└───┘└┘└─────────────────────┘└─
doc         └────┘     └┘                       └─
txt         └────┘     └┘                       └─
par         └────┘     └┘                       └─
pid                  └┘                       
st         └──────────────────────────────────────
684    ... = _ : by rw [f_eq, g_eq]
id                      └──┘  └──┘
src  ─┘             └──┘    └┘    └─
typ  ─┘             └──┘└──┘└┘└──┘└─
doc  ─┘             └──┘    └┘    └─
txt  ─┘             └──┘    └┘    └─
par  ─┘             └──┘    └┘    └─
pid  ─┘               └┘    └┘    
st   ─┘            └───────┘└────┘
685  
src  
typ  
doc  
txt  
par  
pid  
st   
686  lemma sum_sub_index [Π i, add_comm_group (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                            └────────────┘           └────────────┘  └┘       
src                            └────────────┘              └────────────┘  └┘
typ                           └────────────┘           └────────────┘  └┘       
687    [add_comm_group γ] {f g : Π₀ i, β i}
id      └────────────┘          └┘   
src     └────────────┘           └┘  
typ     └────────────┘          └┘   
688    {h : Π i, β i → γ} (h_sub : ∀i b₁ b₂, h i (b₁ - b₂) = h i b₁ - h i b₂) :
id                               └┘ └┘     └┘  └┘     └┘    └┘
src                                                               
typ                              └┘ └┘     └┘  └┘     └┘    └┘
689    (f - g).sum h = f.sum h - g.sum h :=
id         └─┘    └──┘   └──┘ 
src          └─┘      └──┘     └──┘
typ        └─┘    └──┘   └──┘ 
doc           └─┘       └──┘      └──┘
690  have h_zero : ∀i, h i 0 = 0,
id                        
src                          
typ                       
691    from assume i,
id                 
typ                
692    have h i (0 - 0) = h i 0 - h i 0, from h_sub i 0 0,
id                                   └───┘ 
src                           
typ                                  └───┘ 
693    by simpa using this,
id                    └──┘
src       └──────────┘
typ       └──────────┘└──┘
doc       └──────────┘
txt       └──────────┘
par       └──────────┘
pid            └────┘
st       └───────────────┘
694  have h_neg : ∀i b, h i (- b) = - h i b,
id                              
src                               
typ                             
695    from assume i b,
id                  
typ                 
696    have h i (0 - b) = h i 0 - h i b, from h_sub i 0 b,
id                                 └───┘    
src                           
typ                                └───┘    
697    by simpa [h_zero] using this,
id               └────┘        └──┘
src       └─────┘      └──────┘
typ       └─────┘└────┘└──────┘└──┘
doc       └─────┘      └──────┘
txt       └─────┘      └──────┘
par       └─────┘      └──────┘
pid                  └────┘
st       └────────────────────────┘
698  have h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ + h i b₂,
id                  └┘ └┘     └┘  └┘     └┘    └┘
src                                              
typ                 └┘ └┘     └┘  └┘     └┘    └┘
699    from assume i b₁ b₂,
id                  └┘ └┘
typ                 └┘ └┘
700    have h i (b₁ - (- b₂)) = h i b₁ - h i (- b₂), from h_sub i b₁ (-b₂),
id             └┘    └┘      └┘      └┘        └───┘  └┘  └┘
src                                                              
typ            └┘    └┘      └┘      └┘        └───┘  └┘  └┘
701    by simpa [h_neg] using this,
id               └───┘        └──┘
src       └─────┘     └──────┘
typ       └─────┘└───┘└──────┘└──┘
doc       └─────┘     └──────┘
txt       └─────┘     └──────┘
par       └─────┘     └──────┘
pid                 └────┘
st       └───────────────────────┘
702  by simp [@sum_add_index ι β _ γ _ _ _ f (-g) h h_zero h_add];
id             └───────────┘                 └────┘ └───┘
src     └────┘ └───────────┘  └─┘ └─────┘   └┘            
typ     └────┘ └───────────┘└─┘└─────┘ └┘└────┘└───┘
doc     └────┘                └─┘ └─────┘    └┘            
txt     └────┘                └─┘ └─────┘    └┘            
par     └────┘                └─┘ └─────┘    └┘            
pid                         └─┘ └─────┘    └┘            
st     └───────────────────────────────────────────────────────────
703  simp [@sum_neg_index ι β _ γ _ _ _ g h h_zero, h_neg];
id          └───────────┘              └────┘  └───┘
src  └────┘ └───────────┘  └─┘ └─────┘        └┘     
typ  └────┘ └───────────┘└─┘└─────┘└────┘└┘└───┘
doc  └────┘                └─┘ └─────┘        └┘     
txt  └────┘                └─┘ └─────┘        └┘     
par  └────┘                └─┘ └─────┘        └┘     
pid                      └─┘ └─────┘        └┘     
st   ───────────────────────────────────────────────────────
704  simp [@sum_neg ι β _ γ _ _ _ g h]
id          └─────┘             
src  └────┘ └─────┘  └─┘ └─────┘  └─
typ  └────┘ └─────┘└─┘└─────┘└─
doc  └────┘          └─┘ └─────┘  └─
txt  └────┘          └─┘ └─────┘  └─
par  └────┘          └─┘ └─────┘  └─
pid                └─┘ └─────┘  
st   ──────────────────────────────────
705  
src  
typ  
doc  
txt  
par  
pid  
st   
706  @[to_additive]
doc    └─────────┘
707  lemma prod_finset_sum_index {γ : Type w} {α : Type x}
708    [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id          └─────────────┘           └────────────┘  └┘       
src          └─────────────┘              └────────────┘  └┘
typ         └─────────────┘           └────────────┘  └┘       
709    [comm_monoid γ] [decidable_eq α]
id      └─────────┘    └──────────┘ 
src     └─────────┘     └──────────┘
typ     └─────────┘    └──────────┘ 
710    {s : finset α} {g : α → Π₀ i, β i}
id          └────┘           └┘   
src         └────┘             └┘  
typ         └────┘           └┘   
doc         └────┘
711    {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
id                                                    └┘ └┘     └┘  └┘     └┘    └┘
src                                                                                       
typ                                                   └┘ └┘     └┘  └┘     └┘    └┘
712    s.prod (λi, (g i).prod h) = (s.sum g).prod h :=
id     └───┘        └──┘      └──┘  └──┘  
src     └───┘           └──┘        └──┘   └──┘
typ    └───┘        └──┘      └──┘  └──┘  
doc     └───┘           └──┘                └──┘
713  finset.induction_on s
id   └─────────────────┘ 
src  └─────────────────┘
typ  └─────────────────┘ 
doc  └─────────────────┘
714    (by simp [prod_zero_index])
id               └─────────────┘
src        └────┘└─────────────┘
typ        └────┘└─────────────┘
doc        └────┘               
txt        └────┘               
par        └────┘               
pid                           
st        └─────────────────────┘
715    (by simp [prod_add_index, h_zero, h_add] {contextual := tt})
id               └────────────┘  └────┘  └───┘                 └┘
src        └────┘└────────────┘└┘      └┘     └┘ └────────────┘└┘
typ        └────┘└────────────┘└┘└────┘└┘└───┘└┘ └────────────┘└┘
doc        └────┘              └┘      └┘     └┘ └────────────┘  
txt        └────┘              └┘      └┘     └┘ └────────────┘  
par        └────┘              └┘      └┘     └┘ └────────────┘  
pid                          └┘      └┘      └────────────┘  
st        └──────────────────────────────────────────────────────┘
716  
717  @[to_additive]
doc    └─────────┘
718  lemma prod_sum_index  {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁}
id                                         └──────────┘ └┘        └┘
src                                        └──────────┘
typ                                        └──────────┘ └┘        └┘
719    [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))]
id        └┘  └──────┘  └┘ └┘        └────────────┘  └┘      └┘ 
src           └──────┘                └────────────┘  └┘
typ       └┘  └──────┘  └┘ └┘        └────────────┘  └┘      └┘ 
720    [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id          └─────────────┘           └────────────┘  └┘       
src          └─────────────┘              └────────────┘  └┘
typ         └─────────────┘           └────────────┘  └┘       
721    [comm_monoid γ]
id      └─────────┘ 
src     └─────────┘
typ     └─────────┘ 
722    {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i}
id          └┘ └┘ └┘ └┘         └┘  └┘ └┘   └┘   
src         └┘                              └┘  
typ         └┘ └┘ └┘ └┘         └┘  └┘ └┘   └┘   
723    {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
id                                                    └┘ └┘     └┘  └┘     └┘    └┘
src                                                                                       
typ                                                   └┘ └┘     └┘  └┘     └┘    └┘
724    (f.sum g).prod h = f.prod (λi b, (g i b).prod h) :=
id      └──┘  └──┘    └───┘          └──┘  
src      └──┘   └──┘      └───┘               └──┘
typ     └──┘  └──┘    └───┘          └──┘  
doc      └──┘   └──┘       └───┘               └──┘
725  (prod_finset_sum_index h_zero h_add).symm
id    └───────────────────┘ └────┘ └───┘ └──┘
src   └───────────────────┘              └──┘
typ   └───────────────────┘ └────┘ └───┘ └──┘
726  
727  @[simp] lemma sum_single [Π i, add_comm_monoid (β i)]
id                                 └─────────────┘   
src                                 └─────────────┘
typ                                └─────────────┘   
doc    └──┘
728    [Π i, decidable_pred (eq (0 : β i))] {f : Π₀ i, β i} :
id          └────────────┘  └┘                └┘   
src          └────────────┘  └┘                  └┘  
typ         └────────────┘  └┘                └┘   
729    f.sum single = f :=
id     └──┘ └────┘  
src     └──┘ └────┘ 
typ    └──┘ └────┘  
doc     └──┘
730  begin
st   └─────
731    apply dfinsupp.induction f, {rw [sum_zero_index]},
id           └────────────────┘        └────────────┘
src    └────┘└────────────────┘    └──┘└────────────┘
typ    └────┘└────────────────┘   └──┘└────────────┘
doc    └────┘                      └──┘              
txt    └────┘                      └──┘              
par    └────┘                      └──┘              
pid                                 └┘              
st   ───────────────────────────┘└─────┘└────────────┘└─┘
732    intros i b f H hb ih,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid          └────────────┘
st   ─────────────────────┘└─
733    rw [sum_add_index, ih, sum_single_index],
id         └───────────┘  └┘  └──────────────┘
src    └──┘└───────────┘└┘  └┘└──────────────┘
typ    └──┘└───────────┘└┘└┘└┘└──────────────┘
doc    └──┘             └┘  └┘                
txt    └──┘             └┘  └┘                
par    └──┘             └┘  └┘                
pid      └┘             └┘  └┘                
st   ──────────────────┘└──┘└────────────────┘
734    all_goals { intros, simp }
src                             
typ                             
doc                             
txt                             
par                             
pid                             
st                              
735  end
st   └─┘
736  
737  @[to_additive]
doc    └─────────┘
738  lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                                        └──────┘           └────────────┘  └┘       
src                                        └──────┘              └────────────┘  └┘
typ                                       └──────┘           └────────────┘  └┘       
739    [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p]
id      └─────────┘        └┘                    └────────────┘ 
src     └─────────┘         └┘                        └────────────┘
typ     └─────────┘        └┘                    └────────────┘ 
740    {h : Π i, β i → γ} (hp : ∀x∈v.support, p x) :
id                            └──────┘   
src                                 └──────┘
typ                           └──────┘   
741    (v.subtype_domain p).prod (λi b, h i.1 b) = v.prod h :=
id      └─────────────┘  └──┘             └───┘ 
src      └─────────────┘   └──┘                   └───┘
typ     └─────────────┘  └──┘             └───┘ 
doc      └─────────────┘   └──┘                     └───┘
742  finset.prod_bij (λp _, p.val)
id   └─────────────┘      └──┘
src  └─────────────┘         └──┘
typ  └─────────────┘      └──┘
743    (by simp)
744    (by simp)
745    (assume ⟨a₀, ha₀⟩ ⟨a₁, ha₁⟩, by simp)
id                      
typ                     
746    (λ i hi, ⟨⟨i, hp i hi⟩, by simpa using hi, rfl⟩)
id         └┘      └┘  └┘                  └┘  └─┘
src                                               └─┘
typ        └┘      └┘  └┘                  └┘  └─┘
st                                           └┘
747  
748  lemma subtype_domain_sum [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id                                 └─────────────┘           └────────────┘  └┘       
src                                 └─────────────┘              └────────────┘  └┘
typ                                └─────────────┘           └────────────┘  └┘       
749    {s : finset γ} {h : γ → Π₀ i, β i} {p : ι → Prop} [decidable_pred p] :
id          └────┘           └┘                    └────────────┘ 
src         └────┘             └┘                        └────────────┘
typ         └────┘           └┘                    └────────────┘ 
doc         └────┘
750    (s.sum h).subtype_domain p = s.sum (λc, (h c).subtype_domain p) :=
id      └──┘  └────────────┘    └──┘        └────────────┘  
src      └──┘   └────────────┘      └──┘           └────────────┘
typ     └──┘  └────────────┘    └──┘        └────────────┘  
doc             └────────────┘                      └────────────┘
751  eq.symm (s.sum_hom _)
id   └─────┘  └──────┘
src  └─────┘   └──────┘
typ  └─────┘  └──────┘
752  
753  lemma subtype_domain_finsupp_sum {δ : γ → Type x} [decidable_eq γ]
id                                                     └──────────┘ 
src                                                     └──────────┘
typ                                                    └──────────┘ 
754    [Π c, has_zero (δ c)] [Π c, decidable_pred (eq (0 : δ c))]
id          └──────┘           └────────────┘  └┘       
src          └──────┘              └────────────┘  └┘
typ         └──────┘           └────────────┘  └┘       
755    [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id          └─────────────┘           └────────────┘  └┘       
src          └─────────────┘              └────────────┘  └┘
typ         └─────────────┘           └────────────┘  └┘       
756    {p : ι → Prop} [decidable_pred p]
id                    └────────────┘ 
src                    └────────────┘
typ                   └────────────┘ 
757    {s : Π₀ c, δ c} {h : Π c, δ c → Π₀ i, β i} :
id          └┘                  └┘   
src         └┘                        └┘  
typ         └┘                  └┘   
758    (s.sum h).subtype_domain p = s.sum (λc d, (h c d).subtype_domain p) :=
id      └──┘  └────────────┘    └──┘          └────────────┘  
src      └──┘   └────────────┘      └──┘               └────────────┘
typ     └──┘  └────────────┘    └──┘          └────────────┘  
doc      └──┘   └────────────┘       └──┘               └────────────┘
759  subtype_domain_sum
760  
761  end prod_and_sum
762  
763  end dfinsupp